:: CARD_5  semantic presentation begin  

















begin  















theorem :: CARD_5:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_card_1 :::"nextcard"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "X"))))) ; 
 
theorem :: CARD_5:2 (Bool  "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set (Var "f")))) "iff" (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))  ")" ))  ")" ))) ; 
 
theorem :: CARD_5:3 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "holds" (Bool (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "A"))) "is"   ($#v1_finset_1 :::"infinite"::: )  )) ; 
 
theorem :: CARD_5:4 (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "M")) "is"   ($#v1_finset_1 :::"infinite"::: )  )) "holds"  (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "M"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "A")))))) ; 
 registrationlet "phi" be   ($#m1_hidden :::"Ordinal-Sequence":::); 
cluster (Set   ($#k3_card_3 :::"Union"::: )  "phi") ->   ($#v3_ordinal1 :::"ordinal"::: )   ; 
end; 
theorem :: CARD_5:5 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool  "ex" (Set (Var "phi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "phi"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_wellord1 :::"canonical_isomorphism_of"::: )   "(" (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")) ")" ) ")" ) ")" ) "," (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")) ")" ) ")" )) & (Bool (Set (Var "phi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "phi")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")) ")" ))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "phi")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" )))) ; 
 
theorem :: CARD_5:6 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X")))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")) ")" ))))) ; 
 
theorem :: CARD_5:7 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")) ")" ) ")" ))))) ; 
 
theorem :: CARD_5:8 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) (Bool  "ex" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))) & (Bool (Set (Var "A"))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set (Var "B")))  ")" ))) ; 
 
theorem :: CARD_5:9 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) (Bool  "ex" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::) "st"  (Bool  "("  (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "A")))) & (Bool (Set (Var "A"))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set (Var "M"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))  ")" )  ")" ))) ; 
 
theorem :: CARD_5:10 (Bool  "for" (Set (Var "phi")) "," (Set (Var "psi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "phi")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "psi")))) & (Bool (Set (Var "phi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set (Var "psi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  )) "holds"  (Bool (Set (Var "phi"))  ($#r1_hidden :::"="::: )  (Set (Var "psi")))) ; 
 
theorem :: CARD_5:11 (Bool  "for" (Set (Var "phi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "phi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  )) "holds"  (Bool (Set (Var "phi")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) ; 
 
theorem :: CARD_5:12 (Bool  "for" (Set (Var "phi")) "," (Set (Var "psi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"  (Bool (Set (Set  "(" (Set (Var "phi"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "psi")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "phi")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "phi")))) ; 
 
theorem :: CARD_5:13 (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_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set (Var "Y")) where Y "is"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) : (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  "}"  )  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set  "("  ($#k3_card_2 :::"exp"::: )   "(" (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" ) "," (Set (Var "M")) ")"  ")" ))))) ; 
 
theorem :: CARD_5:14 (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Num 2) "," (Set (Var "M")) ")" ))) ; 
 registration
cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )     ($#v1_finset_1 :::"infinite"::: )     ($#v1_card_1 :::"cardinal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster   ($#v1_finset_1 :::"infinite"::: )    ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_hidden :::"set"::: )  ; 
end; definitionmode Aleph is   ($#v1_finset_1 :::"infinite"::: )    ($#m1_hidden :::"Cardinal":::); let "M" be   ($#m1_hidden :::"Cardinal":::); func  :::"cf"::: "M" ->   ($#m1_hidden :::"Cardinal":::) means :: CARD_5:def 1 (Bool  "("  (Bool "M"  ($#r2_ordinal2 :::"is_cofinal_with"::: )  it) & (Bool  "("   "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool "M"  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set (Var "N")))) "holds"  (Bool it  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" )  ")" ); let "N" be   ($#m1_hidden :::"Cardinal":::); func "N" :::"-powerfunc_of"::: "M" ->   ($#m1_hidden :::"Cardinal-Function":::) means :: CARD_5:def 2 (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it)) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "M") & (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Cardinal":::))  ")" )  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "K"))  ($#r2_hidden :::"in"::: )  "M")) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," "N" ")" ))  ")" )  ")" ); end; 











:: deftheorem    defines :::"cf"::: CARD_5:def 1 :  (Bool  "for" (Set (Var "M")) "," (Set (Var "b2")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_5 :::"cf"::: )  (Set (Var "M")))) "iff" (Bool  "("  (Bool (Set (Var "M"))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set (Var "b2"))) & (Bool  "("   "for" (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "M"))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set (Var "N")))) "holds"  (Bool (Set (Var "b2"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" )  ")" )  ")" )); 
 
:: deftheorem    defines :::"-powerfunc_of"::: CARD_5:def 2 :  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"Cardinal-Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "N"))  ($#k2_card_5 :::"-powerfunc_of"::: )  (Set (Var "M")))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b3")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Cardinal":::))  ")" )  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "K"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Set (Var "N")) ")" ))  ")" )  ")" )  ")" ))); 
 registrationlet "A" be   ($#m1_hidden :::"Ordinal":::); 
cluster (Set   ($#k3_card_1 :::"alef"::: )  "A") ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; begin  




theorem :: CARD_5:15 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::) (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_1 :::"alef"::: )  (Set (Var "A")))))) ; 
 
theorem :: CARD_5:16 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::) "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 1)) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Num 2)) & (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "n")))) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "a"))) & (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r1_ordinal1 :::"c="::: )  (Set (Var "a")))  ")" ))) ; 
 
theorem :: CARD_5:17 (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "a"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M"))) "or" (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" )) "holds"  (Bool (Set (Var "M")) "is"   ($#m1_hidden :::"Aleph":::)))) ; 
 
theorem :: CARD_5:18 (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "a"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M"))) "or" (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "M"))) & (Bool (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "M"))) & (Bool (Set (Set (Var "a"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "M"))) & (Bool (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "M")))  ")" ))) ; 
 
theorem :: CARD_5:19 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "a"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" )) ; 
 
theorem :: CARD_5:20 (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::) "holds"  (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "M")) "," (Set (Var "a")) ")" )))) ; 
 
theorem :: CARD_5:21 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 registrationlet "a" be   ($#m1_hidden :::"Aleph":::); let "M" be   ($#m1_hidden :::"Cardinal":::); 
cluster (Set "a"  ($#k1_card_2 :::"+`"::: )  "M") ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; registrationlet "M" be   ($#m1_hidden :::"Cardinal":::); let "a" be   ($#m1_hidden :::"Aleph":::); 
cluster (Set "M"  ($#k1_card_2 :::"+`"::: )  "a") ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; registrationlet "a", "b" be   ($#m1_hidden :::"Aleph":::); 
cluster (Set "a"  ($#k2_card_2 :::"*`"::: )  "b") ->   ($#v1_finset_1 :::"infinite"::: )   ; 

cluster (Set   ($#k3_card_2 :::"exp"::: )   "(" "a" "," "b" ")" ) ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; begin  definitionlet "IT" be   ($#m1_hidden :::"Aleph":::); attr "IT" is  :::"regular":::  means :: CARD_5:def 3 (Bool (Set   ($#k1_card_5 :::"cf"::: )  "IT")  ($#r1_hidden :::"="::: )  "IT"); end; 




:: deftheorem    defines :::"regular"::: CARD_5:def 3 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_hidden :::"Aleph":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_card_5 :::"regular"::: )  ) "iff" (Bool (Set   ($#k1_card_5 :::"cf"::: )  (Set (Var "IT")))  ($#r1_hidden :::"="::: )  (Set (Var "IT")))  ")" )); 
 notationlet "IT" be   ($#m1_hidden :::"Aleph":::); antonym  :::"irregular"::: "IT" for  :::"regular"::: ; end; registrationlet "a" be   ($#m1_hidden :::"Aleph":::); 
cluster (Set   ($#k2_card_1 :::"nextcard"::: )  "a") ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; 
theorem :: CARD_5:22 (Bool (Set   ($#k1_card_5 :::"cf"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) ; 
 
theorem :: CARD_5:23 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::) "holds"  (Bool (Set   ($#k1_card_5 :::"cf"::: )  (Set  "("  ($#k2_card_1 :::"nextcard"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "a"))))) ; 
 
theorem :: CARD_5:24 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::) "holds"  (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_5 :::"cf"::: )  (Set (Var "a"))))) ; 
 
theorem :: CARD_5:25 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set   ($#k1_card_5 :::"cf"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_card_5 :::"cf"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: CARD_5:26 (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"))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_5 :::"cf"::: )  (Set (Var "M"))))) "holds"  (Bool  "("  (Bool (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) & (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" ))) ; 
 
theorem :: CARD_5:27 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "phi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "phi")))  ($#r1_hidden :::"="::: )  (Set (Var "M"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "phi")))  ($#r1_tarski :::"c="::: )  (Set (Var "N"))) & (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_5 :::"cf"::: )  (Set (Var "N"))))) "holds"  (Bool  "("  (Bool (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "phi")))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) & (Bool (Set   ($#k3_card_3 :::"Union"::: )  (Set (Var "phi")))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))  ")" ))) ; 
 registrationlet "a" be   ($#m1_hidden :::"Aleph":::); 
cluster (Set   ($#k1_card_5 :::"cf"::: )  "a") ->   ($#v1_finset_1 :::"infinite"::: )   ; 
end; 
theorem :: CARD_5:28 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::)  "st" (Bool (Bool (Set   ($#k1_card_5 :::"cf"::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Var "a")) "is"   ($#v2_card_1 :::"limit_cardinal"::: )  )) ; 
 
theorem :: CARD_5:29 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::)  "st" (Bool (Bool (Set   ($#k1_card_5 :::"cf"::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))) "holds"  (Bool  "ex" (Set (Var "xi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "xi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_5 :::"cf"::: )  (Set (Var "a")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "xi")))  ($#r1_tarski :::"c="::: )  (Set (Var "a"))) & (Bool (Set (Var "xi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "xi")))) & (Bool (Set (Var "xi")) "is"   ($#m1_hidden :::"Cardinal-Function":::)) & (Bool (Bool  "not" (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "xi")))))  ")" ))) ; 
 
theorem :: CARD_5:30 (Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::) "holds"   (Bool  "("  (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  ) "is"   ($#v1_card_5 :::"regular"::: )  ) & (Bool (Set   ($#k2_card_1 :::"nextcard"::: )  (Set (Var "a"))) "is"   ($#v1_card_5 :::"regular"::: )  )  ")" )) ; 
 begin  




theorem :: CARD_5:31 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Aleph":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Num 2) "," (Set (Var "b")) ")" ))) ; 
 
theorem :: CARD_5:32 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Aleph":::) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set  "("  ($#k2_card_1 :::"nextcard"::: )  (Set (Var "a")) ")" ) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" )  ($#k2_card_2 :::"*`"::: )  (Set  "("  ($#k2_card_1 :::"nextcard"::: )  (Set (Var "a")) ")" )))) ; 
 
theorem :: CARD_5:33 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#m1_hidden :::"Aleph":::) "holds"  (Bool (Set   ($#k6_card_3 :::"Sum"::: )  (Set  "(" (Set (Var "b"))  ($#k2_card_5 :::"-powerfunc_of"::: )  (Set (Var "a")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))) ; 
 
theorem :: CARD_5:34 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Aleph":::)  "st" (Bool (Bool (Set (Var "a")) "is"   ($#v2_card_1 :::"limit_cardinal"::: )  ) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_5 :::"cf"::: )  (Set (Var "a"))))) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_card_3 :::"Sum"::: )  (Set  "(" (Set (Var "b"))  ($#k2_card_5 :::"-powerfunc_of"::: )  (Set (Var "a")) ")" )))) ; 
 
theorem :: CARD_5:35 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"Aleph":::)  "st" (Bool (Bool (Set   ($#k1_card_5 :::"cf"::: )  (Set (Var "a")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set  "("  ($#k6_card_3 :::"Sum"::: )  (Set  "(" (Set (Var "b"))  ($#k2_card_5 :::"-powerfunc_of"::: )  (Set (Var "a")) ")" ) ")" ) "," (Set  "("  ($#k1_card_5 :::"cf"::: )  (Set (Var "a")) ")" ) ")" ))) ; 
 






theorem :: CARD_5:36 (Bool  "for" (Set (Var "O")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "O")))) "holds"  (Bool (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X")))))) ; 
 
theorem :: CARD_5:37 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "O")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "O")))) "holds"  (Bool (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: CARD_5:38 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "O")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r1_tarski :::"c="::: )  (Set (Var "O")))) "holds"  (Bool (Set   ($#k3_wellord1 :::"canonical_isomorphism_of"::: )   "(" (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ) ")" ) "," (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "x")))))) ; 
 registrationlet "O" be   ($#m1_hidden :::"Ordinal":::); let "X" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "O")); let "n" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set (Set  "("  ($#k3_wellord1 :::"canonical_isomorphism_of"::: )   "(" (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  "X" ")" ) ")" ) ")" ) "," (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  "X" ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  "n") ->   ($#v3_ordinal1 :::"ordinal"::: )   ; 
end; registrationlet "X" be   ($#v6_membered :::"natural-membered"::: )     ($#m1_hidden :::"set"::: )  ; let "n" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set (Set  "("  ($#k3_wellord1 :::"canonical_isomorphism_of"::: )   "(" (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  "X" ")" ) ")" ) ")" ) "," (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  "X" ")" ) ")"  ")" )  ($#k1_funct_1 :::"."::: )  "n") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; 
theorem :: CARD_5:39 (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k4_ordinal1 :::"omega"::: ) ) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "F")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "F")) ")" )))) ;