:: CARD_1  semantic presentation begin  































notationsynonym  :::"0":::  for  :::"{}"::: ; end; definitionlet "IT" be    ($#m1_hidden :::"set"::: )  ; attr "IT" is  :::"cardinal":::  means :: CARD_1:def 1 (Bool  "ex" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool "IT"  ($#r1_hidden :::"="::: )  (Set (Var "B"))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool (Set (Var "B"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "A")))  ")" )  ")" )); end; 




:: deftheorem    defines :::"cardinal"::: CARD_1:def 1 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_card_1 :::"cardinal"::: )  ) "iff" (Bool  "ex" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "IT"))  ($#r1_hidden :::"="::: )  (Set (Var "B"))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool (Set (Var "B"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "A")))  ")" )  ")" ))  ")" )); 
 registration
cluster   ($#v1_card_1 :::"cardinal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionmode Cardinal is   ($#v1_card_1 :::"cardinal"::: )     ($#m1_hidden :::"set"::: )  ; end; registration
cluster   ($#v1_card_1 :::"cardinal"::: )    ->   ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 




theorem :: CARD_1:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "X")) "," (Set (Var "A"))  ($#r2_wellord2 :::"are_equipotent"::: )  ))) ; 
 
theorem :: CARD_1:2 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set (Var "N"))) "iff" (Bool (Set (Var "M")) "," (Set (Var "N"))  ($#r2_wellord2 :::"are_equipotent"::: )  )  ")" )) ; 
 
theorem :: CARD_1:3 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) "iff" (Bool  "("  (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N"))) & (Bool (Set (Var "M"))  ($#r1_hidden :::"<>"::: )  (Set (Var "N")))  ")" )  ")" )) ; 
 
theorem :: CARD_1:4 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) "iff" (Bool (Bool  "not" (Set (Var "N"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M"))))  ")" )) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"card"::: "X" ->   ($#m1_hidden :::"Cardinal":::) means :: CARD_1:def 2 (Bool "X" "," it  ($#r2_wellord2 :::"are_equipotent"::: )  ); projectivity  
(Bool  "for" (Set (Var "b1")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "b2")) "," (Set (Var "b1"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool (Set (Var "b1")) "," (Set (Var "b1"))  ($#r2_wellord2 :::"are_equipotent"::: )  )))
 ; end; 





:: deftheorem    defines :::"card"::: CARD_1:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))) "iff" (Bool (Set (Var "X")) "," (Set (Var "b2"))  ($#r2_wellord2 :::"are_equipotent"::: )  )  ")" ))); 
 registration
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v1_card_1 :::"cardinal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "X" be   ($#v1_xboole_0 :::"empty"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_card_1 :::"card"::: )  "X") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_card_1 :::"card"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: CARD_1:5 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) "iff" (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y"))))  ")" )) ; 
 
theorem :: CARD_1:6 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::)  "st" (Bool (Bool (Set (Var "R")) "is"   ($#v2_wellord1 :::"well-ordering"::: )  )) "holds"  (Bool (Set   ($#k1_relat_1 :::"field"::: )  (Set (Var "R"))) "," (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set (Var "R")))  ($#r2_wellord2 :::"are_equipotent"::: )  )) ; 
 
theorem :: CARD_1:7 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "M")))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M"))))) ; 
 
theorem :: CARD_1:8 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "A")))) ; 
 
theorem :: CARD_1:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))))) ; 
 
theorem :: CARD_1:10 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "X"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  ")" ))  ")" )) ; 
 
theorem :: CARD_1:11 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y"))))) ; 
 
theorem :: CARD_1:12 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "Y"))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f"))))  ")" ))  ")" )) ; 
 
theorem :: CARD_1:13 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Bool  "not" (Set (Var "X")) "," (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "X")))  ($#r2_wellord2 :::"are_equipotent"::: )  ))) ; 
 
theorem :: CARD_1:14 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "X")) ")" )))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"nextcard"::: "X" ->   ($#m1_hidden :::"Cardinal":::) means :: CARD_1:def 3 (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  "X")  ($#r2_hidden :::"in"::: )  it) & (Bool  "("   "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  "X")  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool it  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M")))  ")" )  ")" ); end; 





:: deftheorem    defines :::"nextcard"::: CARD_1:def 3 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) & (Bool  "("   "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool (Set (Var "b2"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M")))  ")" )  ")" )  ")" ))); 
 
theorem :: CARD_1:15 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "X"))))) ; 
 
theorem :: CARD_1:16 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "Y"))))) ; 
 
theorem :: CARD_1:17 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "Y"))))) ; 
 
theorem :: CARD_1:18 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "A"))))) ; 
 


definitionlet "M" be   ($#m1_hidden :::"Cardinal":::); attr "M" is  :::"limit_cardinal":::  means :: CARD_1:def 4 (Bool  "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "holds" (Bool (Bool  "not" "M"  ($#r1_hidden :::"="::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "N")))))); end; 




:: deftheorem    defines :::"limit_cardinal"::: CARD_1:def 4 :  (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set (Var "M")) "is"   ($#v2_card_1 :::"limit_cardinal"::: )  ) "iff" (Bool  "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "holds" (Bool (Bool  "not" (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "N"))))))  ")" )); 
 definitionlet "A" be   ($#m1_hidden :::"Ordinal":::); func  :::"alef"::: "A" ->    ($#m1_hidden :::"set"::: )   means :: CARD_1:def 5 (Bool  "ex" (Set (Var "S")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "S")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "A")) & (Bool (Set (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "A"))) "holds"  (Bool (Set (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "A")) & (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "B")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k4_ordinal2 :::"sup"::: )  (Set  "(" (Set (Var "S"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "B")) ")" ) ")" )))  ")" )  ")" )); end; 





:: deftheorem    defines :::"alef"::: CARD_1:def 5 :  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "A")))) "iff" (Bool  "ex" (Set (Var "S")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "S")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")) ")" ) ($#k1_tarski :::"}"::: ) ) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "B")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k4_ordinal2 :::"sup"::: )  (Set  "(" (Set (Var "S"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "B")) ")" ) ")" )))  ")" )  ")" ))  ")" ))); 
 registrationlet "A" be   ($#m1_hidden :::"Ordinal":::); 
cluster (Set   ($#k3_card_1 :::"alef"::: )  "A") ->   ($#v1_card_1 :::"cardinal"::: )   ; 
end; 
theorem :: CARD_1:19 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k3_card_1 :::"alef"::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set  "("  ($#k3_card_1 :::"alef"::: )  (Set (Var "A")) ")" )))) ; 
 
theorem :: CARD_1:20 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool  "for" (Set (Var "S")) "being"   ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "S")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "S"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "B"))))  ")" )) "holds"  (Bool (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k4_ordinal2 :::"sup"::: )  (Set (Var "S")) ")" ))))) ; 
 
theorem :: CARD_1:21 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) "iff" (Bool (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "B"))))  ")" )) ; 
 
theorem :: CARD_1:22 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) ; 
 
theorem :: CARD_1:23 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B"))) "iff" (Bool (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "B"))))  ")" )) ; 
 
theorem :: CARD_1:24 (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"))) & (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "Z"))) & (Bool (Set (Var "X")) "," (Set (Var "Z"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set (Var "Y")) "," (Set (Var "Z"))  ($#r2_wellord2 :::"are_equipotent"::: )  )  ")" )) ; 
 
theorem :: CARD_1:25 (Bool  "for" (Set (Var "Y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "Y")))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))) & (Bool (Bool  "not" (Set (Var "Y")) "," (Set (Var "X"))  ($#r2_wellord2 :::"are_equipotent"::: )  ))  ")" )) ; 
 
theorem :: CARD_1:26 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "," (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: CARD_1:27 (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) ; 
 
theorem :: CARD_1:28 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r2_wellord2 :::"are_equipotent"::: )  ) "iff" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))  ")" )) ; 
 
theorem :: CARD_1:29 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) "iff" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))  ")" )) ; 
 
theorem :: CARD_1:30 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: CARD_1:31 (Bool  "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "Y")) "," (Set (Var "Y1")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "X1"))) & (Bool (Set (Var "Y"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y1"))) & (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set (Var "X1")) "," (Set (Var "Y1"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X1"))) "," (Set (Set (Var "Y"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y1")))  ($#r2_wellord2 :::"are_equipotent"::: )  )) ; 
 
theorem :: CARD_1:32 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "," (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))  ($#r2_wellord2 :::"are_equipotent"::: )  )) ; 
 
theorem :: CARD_1:33 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Var "X")) "," (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "X")))  ($#r2_wellord2 :::"are_equipotent"::: )  ))) ; 
 
theorem :: CARD_1:34 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "," (Set (Set (Var "Y"))  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))  ($#r2_wellord2 :::"are_equipotent"::: )  )) ; 
 
theorem :: CARD_1:35 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "X"))) "," (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "Y")))  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) ; 
 
theorem :: CARD_1:36 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "holds"  (Bool  "("  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool  "ex" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "m")))))  ")" )) ; 
 
theorem :: CARD_1:37 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))) "holds"  (Bool (Set (Var "x")) "is"   ($#v1_card_1 :::"cardinal"::: )  )) ; 
 registration
cluster   ($#v7_ordinal1 :::"natural"::: )    ->   ($#v1_card_1 :::"cardinal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: CARD_1:38 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set (Var "Y")) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 
theorem :: CARD_1:39 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "n"))) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )) ; 
 
theorem :: CARD_1:40 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "m"))))) "holds"  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) ; 
 
theorem :: CARD_1:41 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "n")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "m")))) "iff" (Bool (Set (Var "n"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "m")))  ")" )) ; 
 
theorem :: CARD_1:42 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "m")))) "iff" (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set (Var "m")))  ")" )) ; 
 
theorem :: CARD_1:43 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "X")) "," (Set (Var "n"))  ($#r2_wellord2 :::"are_equipotent"::: )  ))) ; 
 
theorem :: CARD_1:44 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k2_card_1 :::"nextcard"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "n")) ")" )))) ; 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); :: original: :::"succ"::: redefine func  :::"succ"::: "n" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ); end; definitionlet "X" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; :: original: :::"card"::: redefine func  :::"card"::: "X" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ); end; 
theorem :: CARD_1:45 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "X"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 scheme  :: CARD_1:sch 1 CardinalInd{ P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool P1[(Set (Var "M"))]))
 provided
(Bool P1[(Set   ($#k1_xboole_0 :::"{}"::: )  )])
 and  
(Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool P1[(Set (Var "M"))])) "holds"  (Bool P1[(Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "M")))]))
 and  
(Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "M"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "M")) "is"   ($#v2_card_1 :::"limit_cardinal"::: )  ) & (Bool  "("   "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "N"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool P1[(Set (Var "N"))])  ")" )) "holds"  (Bool P1[(Set (Var "M"))]))
 proof 


end; scheme  :: CARD_1:sch 2 CardinalCompInd{ P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool P1[(Set (Var "M"))]))
 provided
(Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool  "("   "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "N"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool P1[(Set (Var "N"))])  ")" )) "holds"  (Bool P1[(Set (Var "M"))]))
 proof 


end; 
theorem :: CARD_1:46 (Bool (Set   ($#k3_card_1 :::"alef"::: )  (Set  ($#k1_xboole_0 :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) ; 
 registration
cluster (Set   ($#k4_ordinal1 :::"omega"::: )  ) ->   ($#v1_card_1 :::"cardinal"::: )    for   ($#m1_hidden :::"number"::: )  ; 
end; 
theorem :: CARD_1:47 (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) ; 
 registration
cluster (Set   ($#k4_ordinal1 :::"omega"::: )  ) ->   ($#v2_card_1 :::"limit_cardinal"::: )   ; 
end; registration
cluster   ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ); 
end; registration
cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_card_1 :::"cardinal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: CARD_1:48 (Bool  "for" (Set (Var "M")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Cardinal":::) (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "n")))))) ; 
 registrationlet "X" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_card_1 :::"card"::: )  "X") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; registration
cluster (Set   ($#k4_ordinal1 :::"omega"::: )  ) ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; registration
cluster   ($#v1_finset_1 :::"infinite"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "X" be   ($#v1_finset_1 :::"infinite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_card_1 :::"card"::: )  "X") ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; begin  
theorem :: CARD_1:49 (Bool (Num 1)  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) ; 
 
theorem :: CARD_1:50 (Bool (Num 2)  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) )) ; 
 
theorem :: CARD_1:51 (Bool (Num 3)  ($#r1_hidden :::"="::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) "," (Num 2) ($#k1_enumset1 :::"}"::: ) )) ; 
 
theorem :: CARD_1:52 (Bool (Num 4)  ($#r1_hidden :::"="::: )  (Set  ($#k2_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) ($#k2_enumset1 :::"}"::: ) )) ; 
 
theorem :: CARD_1:53 (Bool (Num 5)  ($#r1_hidden :::"="::: )  (Set  ($#k3_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) ($#k3_enumset1 :::"}"::: ) )) ; 
 
theorem :: CARD_1:54 (Bool (Num 6)  ($#r1_hidden :::"="::: )  (Set  ($#k4_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) ($#k4_enumset1 :::"}"::: ) )) ; 
 
theorem :: CARD_1:55 (Bool (Num 7)  ($#r1_hidden :::"="::: )  (Set  ($#k5_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) "," (Num 6) ($#k5_enumset1 :::"}"::: ) )) ; 
 
theorem :: CARD_1:56 (Bool (Num 8)  ($#r1_hidden :::"="::: )  (Set  ($#k6_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) "," (Num 6) "," (Num 7) ($#k6_enumset1 :::"}"::: ) )) ; 
 
theorem :: CARD_1:57 (Bool (Num 9)  ($#r1_hidden :::"="::: )  (Set  ($#k7_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) "," (Num 6) "," (Num 7) "," (Num 8) ($#k7_enumset1 :::"}"::: ) )) ; 
 
theorem :: CARD_1:58 (Bool (Num 10)  ($#r1_hidden :::"="::: )  (Set  ($#k8_enumset1 :::"{"::: ) (Set  ($#k1_xboole_0 :::"0"::: ) ) "," (Num 1) "," (Num 2) "," (Num 3) "," (Num 4) "," (Num 5) "," (Num 6) "," (Num 7) "," (Num 8) "," (Num 9) ($#k8_enumset1 :::"}"::: ) )) ; 
 
theorem :: CARD_1:59 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))) "is"   ($#v1_finset_1 :::"infinite"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f"))) "is"   ($#v1_finset_1 :::"infinite"::: )  )) ; 
 




definitionlet "n" be   ($#m1_hidden :::"Nat":::); func  :::"Segm"::: "n" ->    ($#m1_hidden :::"set"::: )   equals :: CARD_1:def 6 "n"; end; 





:: deftheorem    defines :::"Segm"::: CARD_1:def 6 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k6_card_1 :::"Segm"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))); 
 


definitionlet "n" be   ($#m1_hidden :::"Nat":::); :: original: :::"Segm"::: redefine func  :::"Segm"::: "n" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k4_ordinal1 :::"omega"::: ) ); end; 
theorem :: CARD_1:60 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "n"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "n"))))) ; 
 
theorem :: CARD_1:61 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v1_finset_1 :::"finite"::: )  ) "iff" (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))  ")" )) ; 
 registration
cluster   ($#v7_ordinal1 :::"natural"::: )    ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "A" be   ($#v1_finset_1 :::"infinite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_zfmisc_1 :::"bool"::: )  "A") ->   ($#v1_finset_1 :::"infinite"::: )   ; 
let "B" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) ->   ($#v1_finset_1 :::"infinite"::: )   ; 

cluster (Set  ($#k2_zfmisc_1 :::"[:"::: ) "B" "," "A" ($#k2_zfmisc_1 :::":]"::: ) ) ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; registrationlet "X" be   ($#v1_finset_1 :::"infinite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_finset_1 :::"infinite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  "X"); 
end; registration
cluster   ($#v3_ordinal1 :::"ordinal"::: )     ($#v1_finset_1 :::"finite"::: )    ->   ($#v7_ordinal1 :::"natural"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: CARD_1:62 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )))) ; 
 registrationlet "X" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_wellord2 :::"RelIncl"::: )  "X") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: CARD_1:63 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 
theorem :: CARD_1:64 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "k"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "k"))))) ; 
 begin  definitionlet "N", "X" be    ($#m1_hidden :::"set"::: )  ; attr "X" is "N" :::"-element":::  means :: CARD_1:def 7 (Bool (Set   ($#k1_card_1 :::"card"::: )  "X")  ($#r1_hidden :::"="::: )  "N"); end; 





:: deftheorem    defines :::"-element"::: CARD_1:def 7 :  (Bool  "for" (Set (Var "N")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is" (Set (Var "N"))  ($#v3_card_1 :::"-element"::: )  ) "iff" (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Var "N")))  ")" )); 
 registrationlet "N" be   ($#m1_hidden :::"Cardinal":::); 
cluster "N"  ($#v3_card_1 :::"-element"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster (Set   ($#k1_xboole_0 :::"0"::: )  )  ($#v3_card_1 :::"-element"::: )    ->   ($#v1_xboole_0 :::"empty"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xboole_0 :::"empty"::: )    -> (Set   ($#k1_xboole_0 :::"0"::: )  )  ($#v3_card_1 :::"-element"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k1_tarski :::"{"::: ) "x" ($#k1_tarski :::"}"::: ) ) -> (Num 1)  ($#v3_card_1 :::"-element"::: )   ; 
end; registrationlet "N" be   ($#m1_hidden :::"Cardinal":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )   "N"  ($#v3_card_1 :::"-element"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "N" be   ($#m1_hidden :::"Cardinal":::); let "f" be (Set (Const "N"))  ($#v3_card_1 :::"-element"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set   ($#k9_xtuple_0 :::"dom"::: )  "f") -> "N"  ($#v3_card_1 :::"-element"::: )   ; 
end; registration
cluster (Num 1)  ($#v3_card_1 :::"-element"::: )    ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_zfmisc_1 :::"trivial"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_zfmisc_1 :::"trivial"::: )    -> (Num 1)  ($#v3_card_1 :::"-element"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Num 1)  ($#v3_card_1 :::"-element"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  "X"); 
end; definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; mode Singleton of "X" is (Num 1)  ($#v3_card_1 :::"-element"::: )    ($#m1_subset_1 :::"Subset":::) "of" "X"; end; 
theorem :: CARD_1:65 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Singleton":::) "of" (Set (Var "X")) (Bool  "ex" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "st" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: CARD_1:66 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "Y")))))  ")" )) ; 
 
theorem :: CARD_1:67 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "X")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))))) ; 
 
theorem :: CARD_1:68 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Set (Var "Y"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "X")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: CARD_1:69 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )) ; 
 
theorem :: CARD_1:70 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")) ")" )))) ;