:: RAMSEY_1  semantic presentation begin  















definitionlet "X", "Y" be    ($#m1_hidden :::"set"::: )  ; let "H" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "P" be    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Const "Y")) "," (Set (Const "X")) ")" ); pred "H" :::"is_homogeneous_for"::: "P" means :: RAMSEY_1:def 1 (Bool  "ex" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "P" "st" (Bool (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" "Y" "," "H" ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "p")))); end; 







:: deftheorem    defines :::"is_homogeneous_for"::: RAMSEY_1:def 1 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "P")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "Y")) "," (Set (Var "X")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "H"))  ($#r1_ramsey_1 :::"is_homogeneous_for"::: )  (Set (Var "P"))) "iff" (Bool  "ex" (Set (Var "p")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "P")) "st" (Bool (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "Y")) "," (Set (Var "H")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "p"))))  ")" )))); 
 registrationlet "n" be   ($#m1_hidden :::"Nat":::); let "X" be   ($#v1_finset_1 :::"infinite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" "n" "," "X" ")" ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "X", "Y" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); assume that  
(Bool (Set (Const "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )
 and  
(Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Const "n")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Const "X")))) & (Bool (Bool  "not" (Set (Const "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" )
 and  
(Bool (Bool  "not" (Set (Const "Y")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))
 ; func "f" :::"||^"::: "n" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" "n" "," "X" ")"  ")" ) "," (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" "n" "," "Y" ")"  ")" ) means :: RAMSEY_1:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" "n" "," "X" ")" ) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k7_relat_1 :::".:"::: )  (Set (Var "x"))))); end; 









:: deftheorem    defines :::"||^"::: RAMSEY_1:def 2 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "n")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))) & (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Bool  "not" (Set (Var "Y")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "for" (Set (Var "b5")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "X")) ")"  ")" ) "," (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "Y")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_ramsey_1 :::"||^"::: )  (Set (Var "n")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "X")) ")" ) "holds"  (Bool (Set (Set (Var "b5"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "x")))))  ")" ))))); 
 
theorem :: RAMSEY_1:1 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "n")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))) & (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Bool  "not" (Set (Var "Y")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set  "(" (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "H")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_ramsey_1 :::"||^"::: )  (Set (Var "n")) ")" )  ($#k7_relat_1 :::".:"::: )  (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "H")) ")"  ")" ))))))) ; 
 
theorem :: RAMSEY_1:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"infinite"::: )  ) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))) ; 
 
theorem :: RAMSEY_1:3 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"infinite"::: )  )) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y"))) "is"   ($#v1_finset_1 :::"infinite"::: )  )) ; 
 
theorem :: RAMSEY_1:4 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"infinite"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "Y"))) "is"   ($#v1_finset_1 :::"infinite"::: )  )) ; 
 registrationlet "X" be   ($#v1_finset_1 :::"infinite"::: )     ($#m1_hidden :::"set"::: )  ; let "Y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "X"  ($#k2_xboole_0 :::"\/"::: )  "Y") ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; registrationlet "X" be   ($#v1_finset_1 :::"infinite"::: )     ($#m1_hidden :::"set"::: )  ; let "Y" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set "X"  ($#k4_xboole_0 :::"\"::: )  "Y") ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; 
theorem :: RAMSEY_1:5 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: RAMSEY_1:6 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "X")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) ; 
 
theorem :: RAMSEY_1:7 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "Z")) "," (Set (Var "X")) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "Z")) "," (Set (Var "Y")) ")" ))) ; 
 
theorem :: RAMSEY_1:8 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "Y")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: RAMSEY_1:9 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))  "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Bool  "not" (Set (Var "Y")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v3_funct_1 :::"constant"::: )  ) "iff" (Bool  "ex" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "Y")) "st" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )))  ")" ))) ; 
 
theorem :: RAMSEY_1:10 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool  "ex" (Set (Var "Y")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Var "k")))))) ; 
 
theorem :: RAMSEY_1:11 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "m")) ")" )  ($#k6_newton :::"choose"::: )  (Set (Var "m"))))) ; 
 
theorem :: RAMSEY_1:12 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 1))) "holds"  (Bool (Set (Set (Var "m"))  ($#k1_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "m")) ")" )  ($#k6_newton :::"choose"::: )  (Set (Var "m"))))) ; 
 
theorem :: RAMSEY_1:13 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p1")) "," (Set (Var "p2")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "P")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set (Var "P"))  "st" (Bool (Bool (Set (Var "p1"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Set  "("  ($#k13_eqrel_1 :::"proj"::: )  (Set (Var "P")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p1")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k13_eqrel_1 :::"proj"::: )  (Set (Var "P")) ")" )  ($#k3_funct_2 :::"."::: )  (Set (Var "p2"))))) "holds"  (Bool (Set (Var "p2"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))))) ; 
 begin  
theorem :: RAMSEY_1:14 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "X")) ")"  ")" ) "," (Set (Var "k"))  "st" (Bool (Bool (Set (Var "k"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"infinite"::: )  )) "holds"  (Bool  "ex" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v1_finset_1 :::"infinite"::: )  ) & (Bool (Set (Set (Var "F"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "H")) ")"  ")" )) "is"   ($#v3_funct_1 :::"constant"::: )  )  ")" ))))) ; 
 
theorem :: RAMSEY_1:15 (Bool  "for" (Set (Var "n")) "," (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"infinite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "P")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Set (Var "n")) "," (Set (Var "X")) ")" )  "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Set (Var "k")))) "holds"  (Bool  "ex" (Set (Var "H")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set (Var "H")) "is"   ($#v1_finset_1 :::"infinite"::: )  ) & (Bool (Set (Var "H"))  ($#r1_ramsey_1 :::"is_homogeneous_for"::: )  (Set (Var "P")))  ")" ))))) ; 
 begin  scheme  :: RAMSEY_1:sch 1 BinInd2{ P1[  ($#m1_hidden :::"Nat":::) ","   ($#m1_hidden :::"Nat":::)] } : 
(Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "m")) "," (Set (Var "n"))]))
 provided
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool P1[(Set   ($#k6_numbers :::"0"::: )  ) "," (Set (Var "n"))]) & (Bool P1[(Set (Var "n")) "," (Set   ($#k6_numbers :::"0"::: )  )])  ")" ))
 and  
(Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool P1[(Set (Set (Var "m"))  ($#k1_nat_1 :::"+"::: )  (Num 1)) "," (Set (Var "n"))]) & (Bool P1[(Set (Var "m")) "," (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))])) "holds"  (Bool P1[(Set (Set (Var "m"))  ($#k1_nat_1 :::"+"::: )  (Num 1)) "," (Set (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1))]))
 proof 


end; 
theorem :: RAMSEY_1:16 (Bool  "for" (Set (Var "m")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">="::: )  (Num 2))) "holds"  (Bool  "ex" (Set (Var "r")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "(" (Set  "(" (Set (Var "m"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "n")) ")" )  ($#k7_nat_d :::"-'"::: )  (Num 2) ")" )  ($#k6_newton :::"choose"::: )  (Set  "(" (Set (Var "m"))  ($#k7_nat_d :::"-'"::: )  (Num 1) ")" ))) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">="::: )  (Num 2)) & (Bool  "("   "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Num 2) "," (Set (Var "X")) ")"  ")" ) "," (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Num 2) ")" )  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "r")))) "holds"  (Bool  "ex" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "S")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "F"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Num 2) "," (Set (Var "S")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ))  ")" ) "or" (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "S")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "n"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "F"))  ($#k2_partfun1 :::"|"::: )  (Set  "("  ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Num 2) "," (Set (Var "S")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Num 2) ($#k1_tarski :::"}"::: ) ))  ")" )  ")" )))  ")" )  ")" ))) ; 
 
theorem :: RAMSEY_1:17 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "r")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "P")) "being"    ($#m1_eqrel_1 :::"a_partition"::: )   "of" (Set   ($#k3_group_10 :::"the_subsets_of_card"::: )   "(" (Num 2) "," (Set (Var "X")) ")" )  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "r"))) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "P")))  ($#r1_hidden :::"="::: )  (Num 2))) "holds"  (Bool  "ex" (Set (Var "S")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st"  (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "S")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "m"))) & (Bool (Set (Var "S"))  ($#r1_ramsey_1 :::"is_homogeneous_for"::: )  (Set (Var "P")))  ")" )))))) ;