:: CARD_2  semantic presentation begin  






























theorem :: CARD_2:1 (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 "X")) "," (Set (Var "Y"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y"))))  ")" )) ; 
 
theorem :: CARD_2:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "X"))) "," (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" ))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" ) ")" )))  ")" )) ; 
 
theorem :: CARD_2:3 (Bool  "for" (Set (Var "Z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Z"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds"  (Bool  "("  (Bool (Set (Var "Z")) "," (Set (Var "X"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Z")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))  ")" )) ; 
 definitionlet "M", "N" be   ($#m1_hidden :::"Cardinal":::); func "M" :::"+`"::: "N" ->   ($#m1_hidden :::"Cardinal":::) equals :: CARD_2:def 1 (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" "M"  ($#k10_ordinal2 :::"+^"::: )  "N" ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "M"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "N")) ")" )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "N"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "M")) ")" ))))
 ; func "M" :::"*`"::: "N" ->   ($#m1_hidden :::"Cardinal":::) equals :: CARD_2:def 2 (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) "M" "," "N" ($#k2_zfmisc_1 :::":]"::: ) )); commutativity  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "M")) "," (Set (Var "N")) ($#k2_zfmisc_1 :::":]"::: ) )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "N")) "," (Set (Var "M")) ($#k2_zfmisc_1 :::":]"::: ) ))))
 ; func  :::"exp":::  "(" "M" "," "N" ")"  ->   ($#m1_hidden :::"Cardinal":::) equals :: CARD_2:def 3 (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_funct_2 :::"Funcs"::: )   "(" "N" "," "M" ")"  ")" )); end; 


















:: deftheorem    defines :::"+`"::: CARD_2:def 1 :  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "M"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "N")) ")" )))); 
 
:: deftheorem    defines :::"*`"::: CARD_2:def 2 :  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "M")) "," (Set (Var "N")) ($#k2_zfmisc_1 :::":]"::: ) )))); 
 
:: deftheorem    defines :::"exp"::: CARD_2:def 3 :  (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "M")) "," (Set (Var "N")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_funct_2 :::"Funcs"::: )   "(" (Set (Var "N")) "," (Set (Var "M")) ")"  ")" )))); 
 
theorem :: CARD_2:4 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )) ; 
 
theorem :: CARD_2:5 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Z")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )) ; 
 
theorem :: CARD_2:6 (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_2:7 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" ) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "Y")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "Y")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" ) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "Y")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "Y")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )) ; 
 
theorem :: CARD_2:8 (Bool  "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "Y1"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set (Var "X2")) "," (Set (Var "Y2"))  ($#r2_wellord2 :::"are_equipotent"::: )  )) "holds"  (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )) ; 
 
theorem :: CARD_2:9 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "B"))) "," (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "B")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "B")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )))  ")" ))) ; 
 
theorem :: CARD_2:10 (Bool  "for" (Set (Var "K")) "," (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M"))) "," (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "K")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "M")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "K")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "M")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )))  ")" ))) ; 
 
theorem :: CARD_2:11 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "B"))) "," (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) )))  ")" )) ; 
 
theorem :: CARD_2:12 (Bool  "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "Y1"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set (Var "X2")) "," (Set (Var "Y2"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2"))) & (Bool (Set (Var "y1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y2")))) "holds"  (Bool  "("  (Bool (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "," (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y1")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y2")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y2")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x1")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x2")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y1")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y2")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y2")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )))  ")" )) ; 
 
theorem :: CARD_2:13 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "A")) ")" )  ($#k1_card_2 :::"+`"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: CARD_2:14 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "A")) ")" )  ($#k2_card_2 :::"*`"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: CARD_2:15 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) "," (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Num 1) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )))  ")" )) ; 
 
theorem :: CARD_2:16 (Bool  "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) )) "," (Set (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "X1")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y2")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X1")) "," (Set (Var "X2")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y1")) "," (Set (Var "Y2")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X2")) "," (Set (Var "X1")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y2")) "," (Set (Var "Y1")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )))  ")" )) ; 
 
theorem :: CARD_2:17 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" )  ($#k1_card_2 :::"+`"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set  ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )))) ; 
 
theorem :: CARD_2:18 (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "M")))) ; 
 
theorem :: CARD_2:19 (Bool  "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Set  "(" (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M")) ")" )  ($#k1_card_2 :::"+`"::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set  "(" (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N")) ")" )))) ; 
 
theorem :: CARD_2:20 (Bool  "for" (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: CARD_2:21 (Bool  "for" (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "K")))) ; 
 
theorem :: CARD_2:22 (Bool  "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Set  "(" (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")) ")" )  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set  "(" (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")) ")" )))) ; 
 
theorem :: CARD_2:23 (Bool  "for" (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Num 2)  ($#k2_card_2 :::"*`"::: )  (Set (Var "K")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "K"))))) ; 
 
theorem :: CARD_2:24 (Bool  "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set  "(" (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")) ")" )  ($#k1_card_2 :::"+`"::: )  (Set  "(" (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")) ")" )))) ; 
 
theorem :: CARD_2:25 (Bool  "for" (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Set  ($#k6_numbers :::"0"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: CARD_2:26 (Bool  "for" (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "K"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "K")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: CARD_2:27 (Bool  "for" (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "K"))) & (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Num 1) "," (Set (Var "K")) ")" )  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: CARD_2:28 (Bool  "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Set  "(" (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Set (Var "M")) ")"  ")" )  ($#k2_card_2 :::"*`"::: )  (Set  "("  ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Set (Var "N")) ")"  ")" )))) ; 
 
theorem :: CARD_2:29 (Bool  "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set  "(" (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")) ")" ) "," (Set (Var "N")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Set (Var "N")) ")"  ")" )  ($#k2_card_2 :::"*`"::: )  (Set  "("  ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "M")) "," (Set (Var "N")) ")"  ")" )))) ; 
 
theorem :: CARD_2:30 (Bool  "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Set  "(" (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set  "("  ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Set (Var "M")) ")"  ")" ) "," (Set (Var "N")) ")" ))) ; 
 
theorem :: CARD_2:31 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Num 2) "," (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_zfmisc_1 :::"bool"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: CARD_2:32 (Bool  "for" (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Num 2) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "K"))))) ; 
 
theorem :: CARD_2:33 (Bool  "for" (Set (Var "K")) "," (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set  "(" (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M")) ")" ) "," (Num 2) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "K")) ")" )  ($#k1_card_2 :::"+`"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k2_card_2 :::"*`"::: )  (Set (Var "K")) ")" )  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")) ")" ) ")" )  ($#k1_card_2 :::"+`"::: )  (Set  "(" (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")) ")" )))) ; 
 
theorem :: CARD_2:34 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" )  ($#k1_card_2 :::"+`"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: CARD_2:35 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" )  ($#k1_card_2 :::"+`"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "Y")) ")" )))) ; 
 




theorem :: CARD_2:36 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k8_ordinal3 :::"+^"::: )  (Set (Var "m"))))) ; 
 
theorem :: CARD_2:37 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "n"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n"))  ($#k9_ordinal3 :::"*^"::: )  (Set (Var "m"))))) ; 
 
theorem :: CARD_2:38 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Set (Var "m")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "n")) ")" )  ($#k1_card_2 :::"+`"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "m")) ")" )))) ; 
 
theorem :: CARD_2:39 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "n"))  ($#k4_nat_1 :::"*"::: )  (Set (Var "m")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "n")) ")" )  ($#k2_card_2 :::"*`"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "m")) ")" )))) ; 
 
theorem :: CARD_2:40 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "X")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: CARD_2:41 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "X")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))))) ; 
 
theorem :: CARD_2:42 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Num 1)) "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_2:43 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "X")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: CARD_2:44 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "X")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: CARD_2:45 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "X")) ")" )  ($#k2_nat_1 :::"+"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "Y")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" ) ")" )))) ; 
 
theorem :: CARD_2:46 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "X")) ")" )  ($#k4_nat_1 :::"*"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: CARD_2:47 (Bool  "for" (Set (Var "f")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )))) ; 
 
theorem :: CARD_2:48 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "Y")))) "holds"  (Bool  "("  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Y")))) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "Y"))))  ")" )) ; 
 
theorem :: CARD_2:49 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))) "or" (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y"))))  ")" ) & (Bool (Set (Var "Y")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 










theorem :: CARD_2:50 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Num 2))) ; 
 
theorem :: CARD_2:51 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Num 3))) ; 
 
theorem :: CARD_2:52 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Num 4))) ; 
 
theorem :: CARD_2:53 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Num 5))) ; 
 
theorem :: CARD_2:54 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k4_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) ($#k4_enumset1 :::"}"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Num 6))) ; 
 
theorem :: CARD_2:55 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k5_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) ($#k5_enumset1 :::"}"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Num 7))) ; 
 
theorem :: CARD_2:56 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k6_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "," (Set (Var "x6")) "," (Set (Var "x7")) "," (Set (Var "x8")) ($#k6_enumset1 :::"}"::: ) ))  ($#r1_xxreal_0 :::"<="::: )  (Num 8))) ; 
 
theorem :: CARD_2:57 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Num 2))) ; 
 
theorem :: CARD_2:58 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k1_enumset1 :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Num 3))) ; 
 
theorem :: CARD_2:59 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x2"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x1"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x3"))) & (Bool (Set (Var "x2"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4"))) & (Bool (Set (Var "x3"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x4")))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k2_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) ($#k2_enumset1 :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Num 4))) ; 
 begin  
theorem :: CARD_2:60 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Num 2))) "holds"  (Bool  "ex" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"<>"::: )  (Set (Var "y"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))  ")" ))) ; 
 
theorem :: CARD_2:61 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )))) ; 
 
theorem :: CARD_2:62 (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Z"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "Z")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool  "("   "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Z"))) & (Bool (Bool  "not" (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "Z")))  ($#r2_hidden :::"in"::: )  (Set (Var "Z")))) ; 
 
theorem :: CARD_2:63 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5"))  ($#r3_zfmisc_1 :::"are_mutually_different"::: )  )) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  ($#k3_enumset1 :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x5")) ($#k3_enumset1 :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Num 5))) ; 
 
theorem :: CARD_2:64 (Bool  "for" (Set (Var "M1")) "," (Set (Var "M2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "M1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "M2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "M1"))  ($#r1_hidden :::"="::: )  (Set (Var "M2")))) ; 
 registrationlet "x", "y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set  ($#k4_tarski :::"["::: ) "x" "," "y" ($#k4_tarski :::"]"::: ) ) ->  ($#~v7_ordinal1  "non"   ($#v7_ordinal1 :::"natural"::: )   )  ; 
end; begin  





































theorem :: CARD_2:65 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set   ($#k6_card_3 :::"Sum"::: )  (Set  "(" (Set (Var "M"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "N")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N"))))) ; 
 
theorem :: CARD_2:66 (Bool  "for" (Set (Var "N")) "," (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set   ($#k7_card_3 :::"Product"::: )  (Set  "(" (Set (Var "N"))  ($#k7_funcop_1 :::"-->"::: )  (Set (Var "M")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "M")) "," (Set (Var "N")) ")" ))) ; 
 scheme  :: CARD_2:sch 1 FinRegularity{ F1() ->   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "y"))  ($#r1_hidden :::"<>"::: )  (Set (Var "x")))) "holds"  (Bool  "not" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))]))  ")" )  ")" ))
 provided
(Bool (Set F1 "("  ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))
 and  
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "x"))])) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))
 and  
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "z"))])) "holds"  (Bool P1[(Set (Var "x")) "," (Set (Var "z"))]))
 proof 


end; scheme  :: CARD_2:sch 2 MaxFinSetElem{ F1() ->   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])  ")" )  ")" ))
 provided
(Bool (Set F1 "("  ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))
 and  
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("  (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) "or" (Bool P1[(Set (Var "y")) "," (Set (Var "x"))])  ")" ))
 and  
(Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y")) "," (Set (Var "z"))])) "holds"  (Bool P1[(Set (Var "x")) "," (Set (Var "z"))]))
 proof 


end; 
theorem :: CARD_2:67 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set (Var "n"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 
theorem :: CARD_2:68 (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) "iff" (Bool (Num 1)  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M")))  ")" )) ; 
 
theorem :: CARD_2:69 (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set (Var "M"))) "iff" (Bool (Num 2)  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M")))  ")" )) ; 
 




theorem :: CARD_2:70 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) "iff" (Bool  "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "B"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))))  ")" )) ; 
 
theorem :: CARD_2:71 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" )  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "n")))) & (Bool (Set (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" )  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "n"))))  ")" ))) ; 
 
theorem :: CARD_2:72 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "n")))))) ; 
 
theorem :: CARD_2:73 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) ; 
 
theorem :: CARD_2:74 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r1_ordinal1 :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Num 1)  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) ; 
 registration
cluster   ($#v1_finset_1 :::"infinite"::: )     ($#v1_card_1 :::"cardinal"::: )    ->   ($#v4_ordinal1 :::"limit_ordinal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: CARD_2:75 (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "M")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) "holds"  (Bool (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "M")))) ; 
 
theorem :: CARD_2:76 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "M")) "is"   ($#v1_finset_1 :::"finite"::: )  )) & (Bool  "("  (Bool (Set (Var "N"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M"))) "or" (Bool (Set (Var "N"))  ($#r2_hidden :::"in"::: )  (Set (Var "M")))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N")))  ($#r1_hidden :::"="::: )  (Set (Var "M"))) & (Bool (Set (Set (Var "N"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M")))  ($#r1_hidden :::"="::: )  (Set (Var "M")))  ")" )) ; 
 
theorem :: CARD_2:77 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )) & (Bool  "("  (Bool (Set (Var "X")) "," (Set (Var "Y"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) "or" (Bool (Set (Var "Y")) "," (Set (Var "X"))  ($#r2_wellord2 :::"are_equipotent"::: )  )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y"))) "," (Set (Var "X"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))  ")" )) ; 
 
theorem :: CARD_2:78 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )) & (Bool (Set (Var "Y")) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y"))) "," (Set (Var "X"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))  ")" )) ; 
 
theorem :: CARD_2:79 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_finset_1 :::"finite"::: )  )) & (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))) "or" (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y"))) "," (Set (Var "X"))  ($#r2_wellord2 :::"are_equipotent"::: )  ) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))  ")" )) ; 
 
theorem :: CARD_2:80 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 
theorem :: CARD_2:81 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "M")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) "holds"  (Bool  "("  (Bool (Bool  "not" (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) & (Bool (Bool  "not" (Set (Set (Var "N"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M"))) "is"   ($#v1_finset_1 :::"finite"::: )  ))  ")" )) ; 
 
theorem :: CARD_2:82 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Cardinal":::) "holds"  (Bool (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 
theorem :: CARD_2:83 (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "K"))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "K"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "K"))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "K"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "L"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N")))) & (Bool (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "K")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "L"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N"))))  ")" )) ; 
 
theorem :: CARD_2:84 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) "or" (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N")))) & (Bool (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "N"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "K")))) & (Bool (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "K")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N")))) & (Bool (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "K")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "N"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "K"))))  ")" )) ; 
 
theorem :: CARD_2:85 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v4_card_3 :::"countable"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v4_card_3 :::"countable"::: )  )) "holds"  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y"))) "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 
theorem :: CARD_2:86 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set (Var "f")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")))))) ; 
 
theorem :: CARD_2:87 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "M"))) & (Bool  "("   "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "X")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")))))) ; 
 
theorem :: CARD_2:88 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )) "holds"  (Bool (Set   ($#k3_card_3 :::"Union"::: )  (Set (Var "f"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) ; 
 
theorem :: CARD_2:89 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Set  ($#k4_ordinal1 :::"omega"::: ) )  ($#k2_card_2 :::"*`"::: )  (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "n")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) & (Bool (Set (Set  "("  ($#k5_card_1 :::"card"::: )  (Set (Var "n")) ")" )  ($#k2_card_2 :::"*`"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))  ")" )) ; 
 
theorem :: CARD_2:90 (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "K"))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "K"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "K"))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "K"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" )  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "L"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")))) & (Bool (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "K")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "L"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N"))))  ")" )) ; 
 
theorem :: CARD_2:91 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool  "("  (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N"))) "or" (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")))) & (Bool (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "N"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "K")))) & (Bool (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "K")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")))) & (Bool (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "K")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "N"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "K"))))  ")" )) ; 
 
theorem :: CARD_2:92 (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "holds"  (Bool  "("  (Bool  "("  (Bool  "not" (Bool  "("  (Bool (Set (Var "K"))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "K"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "K"))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" )) & (Bool  "not" (Bool  "("  (Bool (Set (Var "K"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N")))  ")" ))  ")" ) "or" (Bool (Set (Var "K"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Set (Var "M")) ")" )  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "L")) "," (Set (Var "N")) ")" ))  ")" )) ; 
 
theorem :: CARD_2:93 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "," (Set (Var "K")) "being"   ($#m1_hidden :::"Cardinal":::)  "holds"  (Bool  "("  (Bool  "("  (Bool (Bool  "not" (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) & (Bool (Bool  "not" (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "N"))))  ")" ) "or" (Bool (Set (Var "K"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool  "("  (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Set (Var "M")) ")" )  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "K")) "," (Set (Var "N")) ")" )) & (Bool (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "M")) "," (Set (Var "K")) ")" )  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k3_card_2 :::"exp"::: )   "(" (Set (Var "N")) "," (Set (Var "K")) ")" ))  ")" )  ")" )) ; 
 
theorem :: CARD_2:94 (Bool  "for" (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::) "holds"   (Bool  "("  (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N")))) & (Bool (Set (Var "N"))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N"))))  ")" )) ; 
 
theorem :: CARD_2:95 (Bool  "for" (Set (Var "N")) "," (Set (Var "M")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "N"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "M"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N")))) & (Bool (Set (Var "M"))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "N"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M"))))  ")" )) ; 
 
theorem :: CARD_2:96 (Bool  "for" (Set (Var "K")) "," (Set (Var "L")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Var "K"))  ($#r2_hidden :::"in"::: )  (Set (Var "L"))) & (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "L"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N")))) & (Bool (Set (Set (Var "M"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "K")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "L"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N"))))  ")" )) ; 
 
theorem :: CARD_2:97 (Bool  "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "M")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "K"))  ($#k1_card_2 :::"+`"::: )  (Set (Var "N"))))) "holds"  (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) ; 
 
theorem :: CARD_2:98 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "X")) ")" )  ($#k1_card_2 :::"+`"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "(" (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) ; 
 
theorem :: CARD_2:99 (Bool  "for" (Set (Var "K")) "," (Set (Var "M")) "," (Set (Var "N")) "being"   ($#m1_hidden :::"Cardinal":::)  "st" (Bool (Bool (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "M")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "K"))  ($#k2_card_2 :::"*`"::: )  (Set (Var "N"))))) "holds"  (Bool (Set (Var "M"))  ($#r2_hidden :::"in"::: )  (Set (Var "N")))) ; 
 
theorem :: CARD_2:100 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v4_card_3 :::"countable"::: )  ) & (Bool (Set (Var "Y")) "is"   ($#v4_card_3 :::"countable"::: )  )) "holds"  (Bool (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y"))) "is"   ($#v4_card_3 :::"countable"::: )  )) ; 
 registrationlet "A" be   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  ; let "B" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set  "("  ($#k5_finsub_1 :::"Fin"::: )  (Set (Const "B")) ")" ); 
cluster (Set   ($#k3_card_3 :::"Union"::: )  "f") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; registrationlet "f" be   ($#v1_finset_1 :::"finite"::: )     ($#v2_finset_1 :::"finite-yielding"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set   ($#k4_card_3 :::"product"::: )  "f") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: CARD_2:101 (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   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F"))) "is"   ($#v1_finset_1 :::"finite"::: )  )) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F")))) & (Bool (Set (Set (Var "F"))  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "is"   ($#v1_finset_1 :::"infinite"::: )  )  ")" ))) ;