:: CLASSES2  semantic presentation begin  



















registration
cluster   ($#v2_classes1 :::"Tarski"::: )    ->   ($#v1_classes1 :::"subset-closed"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_classes1 :::"Tarski-Class"::: )  "X") ->   ($#v2_classes1 :::"Tarski"::: )   ; 
end; 
theorem :: CLASSES2:1 (Bool  "for" (Set (Var "W")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v1_classes1 :::"subset-closed"::: )  ) & (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool  "("  (Bool (Bool  "not" (Set (Var "X")) "," (Set (Var "W"))  ($#r2_tarski :::"are_equipotent"::: )  )) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W"))))  ")" )) ; 
 
theorem :: CLASSES2:2 (Bool  "for" (Set (Var "W")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool  "("  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "W")))  ")" )) ; 
 
theorem :: CLASSES2:3 (Bool  "for" (Set (Var "W")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) ; 
 
theorem :: CLASSES2:4 (Bool  "for" (Set (Var "W")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set (Var "W")))) ; 
 
theorem :: CLASSES2:5 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "W")))  ")" ))) ; 
 
theorem :: CLASSES2:6 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))) "holds"  (Bool  "("  (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")))) & (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))  ")" ))) ; 
 
theorem :: CLASSES2:7 (Bool  "for" (Set (Var "W")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v1_classes1 :::"subset-closed"::: )  ) & (Bool (Set (Var "X")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) & (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "W")))) ; 
 
theorem :: CLASSES2:8 (Bool  "for" (Set (Var "X")) "," (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) & (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))) ; 
 
theorem :: CLASSES2:9 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  )) "holds"  (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "W")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W"))))) ; 
 
theorem :: CLASSES2:10 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" )))) ; 
 
theorem :: CLASSES2:11 (Bool  "for" (Set (Var "W")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) ; 
 
theorem :: CLASSES2:12 (Bool  "for" (Set (Var "X")) "," (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))) ; 
 
theorem :: CLASSES2:13 (Bool  "for" (Set (Var "W")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W"))))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) ; 
 
theorem :: CLASSES2:14 (Bool  "for" (Set (Var "x")) "," (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" )))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))) ; 
 
theorem :: CLASSES2:15 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W"))))) "holds"  (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))))) ; 
 
theorem :: CLASSES2:16 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" )))) "holds"  (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")))))) ; 
 
theorem :: CLASSES2:17 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set (Var "m"))  ($#r1_tarski :::"c="::: )  (Set (Var "W"))))) ; 
 
theorem :: CLASSES2:18 (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Cardinal":::)  (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "m"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))) "holds"  (Bool (Set (Var "m"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")))))) ; 
 
theorem :: CLASSES2:19 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W"))) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) ; 
 
theorem :: CLASSES2:20 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "W"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W"))) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )  ")" )) ; 
 
theorem :: CLASSES2:21 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" )) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )  ")" )) ; 
 










theorem :: CLASSES2:22 (Bool  "for" (Set (Var "W")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool  "("  (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "W")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )  ")" ) "or" (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "W")))  ")" ) "or" (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W")))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "W")))  ")" )  ")" )) "holds"  (Bool (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set (Var "W")) ")" )  ($#r1_tarski :::"c="::: )  (Set (Var "W")))) ; 
 
theorem :: CLASSES2:23 (Bool  "for" (Set (Var "X")) "," (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("  (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")))) & (Bool (Set (Var "W")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )  ")" ) "or" (Bool  "("  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))  ")" ) "or" (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))  ")" )  ")" )) "holds"  (Bool (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ) ")" )  ($#r1_tarski :::"c="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))) ; 
 
theorem :: CLASSES2:24 (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L"))) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L"))))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_classes1 :::"Rank"::: )  (Set (Var "A"))))  ")" )) "holds"  (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set (Var "L"))))) ; 
 
theorem :: CLASSES2:25 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "W"))))) "holds"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set (Var "A")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W")))) & (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))  ")" ))) ; 
 
theorem :: CLASSES2:26 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" )))) "holds"  (Bool  "("  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set (Var "A")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ))) & (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))  ")" ))) ; 
 
theorem :: CLASSES2:27 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  )) "holds"  (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "W")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Var "W")))) ; 
 
theorem :: CLASSES2:28 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))) ; 
 
theorem :: CLASSES2:29 (Bool  "for" (Set (Var "W")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "W")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) & (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set   ($#k6_classes1 :::"the_rank_of"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) ; 
 
theorem :: CLASSES2:30 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "W")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )) "holds"  (Bool (Set (Var "W"))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "W")) ")" )))) ; 
 
theorem :: CLASSES2:31 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "W")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )) "holds"  (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "W")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "W")))) ; 
 
theorem :: CLASSES2:32 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "W"))))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set (Var "A")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W")))))) ; 
 
theorem :: CLASSES2:33 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" )))) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set (Var "A")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ))))) ; 
 
theorem :: CLASSES2:34 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "W")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "W")) ")" ) ")" )))) ; 
 
theorem :: CLASSES2:35 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ) ")" ) ")" )))) ; 
 
theorem :: CLASSES2:36 (Bool  "for" (Set (Var "W")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "W")) ")" ))) & (Bool (Bool  "not" (Set (Var "X")) "," (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "W")) ")" ))  ($#r2_tarski :::"are_equipotent"::: )  ))) "holds"  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "W")) ")" )))) ; 
 
theorem :: CLASSES2:37 (Bool  "for" (Set (Var "X")) "," (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ) ")" ))) "or" (Bool (Set (Var "X")) "," (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ) ")" ))  ($#r2_tarski :::"are_equipotent"::: )  ) "or" (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ) ")" )))  ")" )) ; 
 
theorem :: CLASSES2:38 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  )) "holds"  (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "W")) ")" )) "is"   ($#v2_classes1 :::"Tarski"::: )  )) ; 
 
theorem :: CLASSES2:39 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ) ")" )) "is"   ($#v2_classes1 :::"Tarski"::: )  )) ; 
 
theorem :: CLASSES2:40 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) & (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_classes1 :::"the_rank_of"::: )  (Set (Var "X"))))) "holds"  (Bool  "ex" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set   ($#k6_classes1 :::"the_rank_of"::: )  (Set (Var "Y")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))  ")" )))) ; 
 
theorem :: CLASSES2:41 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )) "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k6_classes1 :::"the_rank_of"::: )  (Set (Var "X")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set (Var "X"))))) ; 
 
theorem :: CLASSES2:42 (Bool  "for" (Set (Var "W")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v2_classes1 :::"Tarski"::: )  ) & (Bool (Set (Var "X")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) & (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set (Var "W")) ")" )))) ; 
 
theorem :: CLASSES2:43 (Bool  "for" (Set (Var "X")) "," (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) & (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))) "holds"  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ) ")" )))) ; 
 
theorem :: CLASSES2:44 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )) "holds"  (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ) ")" ))  ($#r1_classes1 :::"is_Tarski-Class_of"::: )  (Set (Var "W")))) ; 
 
theorem :: CLASSES2:45 (Bool  "for" (Set (Var "W")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "W")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )) "holds"  (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "W"))))) ; 
 definitionlet "IT" be    ($#m1_hidden :::"set"::: )  ; attr "IT" is  :::"universal":::  means :: CLASSES2:def 1 (Bool  "("  (Bool "IT" "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) & (Bool "IT" "is"   ($#v2_classes1 :::"Tarski"::: )  )  ")" ); end; 




:: deftheorem    defines :::"universal"::: CLASSES2:def 1 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_classes2 :::"universal"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v2_classes1 :::"Tarski"::: )  )  ")" )  ")" )); 
 registration
cluster   ($#v1_classes2 :::"universal"::: )    ->   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_classes1 :::"Tarski"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_classes1 :::"Tarski"::: )    ->   ($#v1_classes2 :::"universal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_classes2 :::"universal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionmode Universe is  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_classes2 :::"universal"::: )     ($#m1_hidden :::"set"::: )  ; end; 





theorem :: CLASSES2:46 (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "U"))) "is"   ($#m1_hidden :::"Ordinal":::))) ; 
 
theorem :: CLASSES2:47 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  )) "holds"  (Bool (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "X"))) "is"   ($#v1_classes2 :::"universal"::: )  )) ; 
 
theorem :: CLASSES2:48 (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "U"))) "is"   ($#m1_hidden :::"Universe":::))) ; 
 registrationlet "U" be   ($#m1_hidden :::"Universe":::); 
cluster (Set   ($#k2_ordinal1 :::"On"::: )  "U") ->   ($#v3_ordinal1 :::"ordinal"::: )   ; 

cluster (Set   ($#k1_classes1 :::"Tarski-Class"::: )  "U") ->   ($#v1_classes2 :::"universal"::: )   ; 
end; 
theorem :: CLASSES2:49 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set (Var "A"))) "is"   ($#v1_classes2 :::"universal"::: )  )) ; 
 registrationlet "A" be   ($#m1_hidden :::"Ordinal":::); 
cluster (Set   ($#k1_classes1 :::"Tarski-Class"::: )  "A") ->   ($#v1_classes2 :::"universal"::: )   ; 
end; 
theorem :: CLASSES2:50 (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set (Var "U"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_classes1 :::"Rank"::: )  (Set  "("  ($#k2_ordinal1 :::"On"::: )  (Set (Var "U")) ")" )))) ; 
 
theorem :: CLASSES2:51 (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "U")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "U"))) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )  ")" )) ; 
 
theorem :: CLASSES2:52 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#m1_hidden :::"Universe":::)  "holds"  (Bool  "("  (Bool (Set (Var "U1"))  ($#r2_hidden :::"in"::: )  (Set (Var "U2"))) "or" (Bool (Set (Var "U1"))  ($#r1_hidden :::"="::: )  (Set (Var "U2"))) "or" (Bool (Set (Var "U2"))  ($#r2_hidden :::"in"::: )  (Set (Var "U1")))  ")" )) ; 
 
theorem :: CLASSES2:53 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#m1_hidden :::"Universe":::)  "holds"  (Bool  "("  (Bool (Set (Var "U1"))  ($#r1_tarski :::"c="::: )  (Set (Var "U2"))) "or" (Bool (Set (Var "U2"))  ($#r2_hidden :::"in"::: )  (Set (Var "U1")))  ")" )) ; 
 
theorem :: CLASSES2:54 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  )) ; 
 
theorem :: CLASSES2:55 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#m1_hidden :::"Universe":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "U1"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "U2"))) "is"   ($#m1_hidden :::"Universe":::)) & (Bool (Set (Set (Var "U1"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "U2"))) "is"   ($#m1_hidden :::"Universe":::))  ")" )) ; 
 
theorem :: CLASSES2:56 (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) ; 
 
theorem :: CLASSES2:57 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "U"))))) ; 
 
theorem :: CLASSES2:58 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool  "("  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "U")))  ")" ))) ; 
 
theorem :: CLASSES2:59 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool  "("  (Bool (Set   ($#k9_setfam_1 :::"bool"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set   ($#k1_setfam_1 :::"meet"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))  ")" ))) ; 
 
theorem :: CLASSES2:60 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Set (Var "X"))  ($#k5_xboole_0 :::"\+\"::: )  (Set (Var "Y")))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))  ")" ))) ; 
 
theorem :: CLASSES2:61 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool  "("  (Bool (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )  ($#r2_hidden :::"in"::: )  (Set (Var "U")))  ")" ))) ; 
 



registrationlet "U1" be   ($#m1_hidden :::"Universe":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" "U1"; 
end; definitionlet "U" be   ($#m1_hidden :::"Universe":::); let "u" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "U")); :: original: :::"{"::: redefine func :::"{":::"u":::"}"::: ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; :: original: :::"bool"::: redefine func  :::"bool"::: "u" ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; :: original: :::"union"::: redefine func  :::"union"::: "u" ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; :: original: :::"meet"::: redefine func  :::"meet"::: "u" ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; let "v" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "U")); :: original: :::"{"::: redefine func :::"{":::"u" "," "v":::"}"::: ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; :: original: :::"["::: redefine func :::"[":::"u" "," "v":::"]"::: ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; :: original: :::"\/"::: redefine func "u" :::"\/"::: "v" ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; :: original: :::"/\"::: redefine func "u" :::"/\"::: "v" ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; :: original: :::"\"::: redefine func "u" :::"\"::: "v" ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; :: original: :::"\+\"::: redefine func "u" :::"\+\"::: "v" ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; :: original: :::"[:"::: redefine func :::"[:":::"u" "," "v":::":]"::: ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; :: original: :::"Funcs"::: redefine func  :::"Funcs":::  "(" "u" "," "v" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" "U"; end; definitionfunc  :::"FinSETS":::  ->   ($#m1_hidden :::"Universe":::) equals :: CLASSES2:def 2 (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) )); end; 




:: deftheorem    defines :::"FinSETS"::: CLASSES2:def 2 :  (Bool (Set   ($#k13_classes2 :::"FinSETS"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))); 
 
theorem :: CLASSES2:62 (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ))) ; 
 
theorem :: CLASSES2:63 (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) )) "is"   ($#v2_classes1 :::"Tarski"::: )  ) ; 
 
theorem :: CLASSES2:64 (Bool (Set   ($#k13_classes2 :::"FinSETS"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k4_classes1 :::"Rank"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ))) ; 
 definitionfunc  :::"SETS":::  ->   ($#m1_hidden :::"Universe":::) equals :: CLASSES2:def 3 (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set  ($#k13_classes2 :::"FinSETS"::: ) )); end; 




:: deftheorem    defines :::"SETS"::: CLASSES2:def 3 :  (Bool (Set   ($#k14_classes2 :::"SETS"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set  ($#k13_classes2 :::"FinSETS"::: ) ))); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k5_classes1 :::"the_transitive-closure_of"::: )  "X") ->   ($#v1_ordinal1 :::"epsilon-transitive"::: )   ; 
end; registrationlet "X" be   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_classes1 :::"Tarski-Class"::: )  "X") ->   ($#v1_ordinal1 :::"epsilon-transitive"::: )   ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"Universe_closure"::: "X" ->   ($#m1_hidden :::"Universe":::) means :: CLASSES2:def 4 (Bool  "("  (Bool "X"  ($#r1_tarski :::"c="::: )  it) & (Bool  "("   "for" (Set (Var "Y")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool "X"  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool it  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  ")" )  ")" ); end; 





:: deftheorem    defines :::"Universe_closure"::: CLASSES2:def 4 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Universe":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k15_classes2 :::"Universe_closure"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "b2"))) & (Bool  "("   "for" (Set (Var "Y")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "b2"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))  ")" )  ")" )  ")" ))); 
 definitionmode FinSet is    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k13_classes2 :::"FinSETS"::: )  ); mode Set is    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k14_classes2 :::"SETS"::: )  ); let "A" be   ($#m1_hidden :::"Ordinal":::); func  :::"UNIVERSE"::: "A" ->    ($#m1_hidden :::"set"::: )   means :: CLASSES2:def 5 (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "L")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "A")) & (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k13_classes2 :::"FinSETS"::: )  )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "A"))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "A")) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_classes2 :::"Universe_closure"::: )  (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" )))  ")" )  ")" )); end; 





:: deftheorem    defines :::"UNIVERSE"::: CLASSES2:def 5 :  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set (Var "A")))) "iff" (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "L")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k13_classes2 :::"FinSETS"::: )  )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_classes2 :::"Universe_closure"::: )  (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" )))  ")" )  ")" ))  ")" ))); 
 registrationlet "A" be   ($#m1_hidden :::"Ordinal":::); 
cluster (Set   ($#k16_classes2 :::"UNIVERSE"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_classes2 :::"universal"::: )   ; 
end; 
theorem :: CLASSES2:65 (Bool (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k13_classes2 :::"FinSETS"::: )  )) ; 
 
theorem :: CLASSES2:66 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set  "("  ($#k16_classes2 :::"UNIVERSE"::: )  (Set (Var "A")) ")" )))) ; 
 
theorem :: CLASSES2:67 (Bool (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k14_classes2 :::"SETS"::: )  )) ; 
 
theorem :: CLASSES2:68 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set (Var "B"))))  ")" )) "holds"  (Bool (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k15_classes2 :::"Universe_closure"::: )  (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set (Var "L")) ")" ))))) ; 
 
theorem :: CLASSES2:69 (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::) "holds"   (Bool  "("  (Bool (Set   ($#k13_classes2 :::"FinSETS"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set (Var "U"))) & (Bool (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_tarski :::"c="::: )  (Set (Var "U")))  ")" )) ; 
 
theorem :: CLASSES2:70 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) "iff" (Bool (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set (Var "B"))))  ")" )) ; 
 
theorem :: CLASSES2:71 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B")))) ; 
 
theorem :: CLASSES2:72 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B"))) "iff" (Bool (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k16_classes2 :::"UNIVERSE"::: )  (Set (Var "B"))))  ")" )) ; 
 




theorem :: CLASSES2:73 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k3_classes1 :::"Tarski-Class"::: )   "(" (Set (Var "X")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_classes1 :::"Tarski-Class"::: )   "(" (Set (Var "X")) "," (Num 1) ")" )) & (Bool (Set   ($#k3_classes1 :::"Tarski-Class"::: )   "(" (Set (Var "X")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k3_classes1 :::"Tarski-Class"::: )   "(" (Set (Var "X")) "," (Num 1) ")" ))  ")" )) ;