:: ORDINAL6  semantic presentation begin  




























definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; attr "X" is  :::"ordinal-membered":::  means :: ORDINAL6:def 1 (Bool  "ex" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool "X"  ($#r1_tarski :::"c="::: )  (Set (Var "a")))); end; 




:: deftheorem    defines :::"ordinal-membered"::: ORDINAL6:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_ordinal6 :::"ordinal-membered"::: )  ) "iff" (Bool  "ex" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "a"))))  ")" )); 
 registration
cluster   ($#v3_ordinal1 :::"ordinal"::: )    ->   ($#v1_ordinal6 :::"ordinal-membered"::: )    for    ($#m1_hidden :::"set"::: )  ; 
let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_ordinal1 :::"On"::: )  "X") ->   ($#v1_ordinal6 :::"ordinal-membered"::: )   ; 
end; 
theorem :: ORDINAL6:1 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_ordinal6 :::"ordinal-membered"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "x")) "is"   ($#v3_ordinal1 :::"ordinal"::: )  ))  ")" )) ; 
 registration
cluster   ($#v1_ordinal6 :::"ordinal-membered"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "X" be   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster   ->   ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "X"; 
end; 
theorem :: ORDINAL6:2 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_ordinal6 :::"ordinal-membered"::: )  ) "iff" (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" )) ; 
 
theorem :: ORDINAL6:3 (Bool  "for" (Set (Var "X")) "being"   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X"))))) ; 
 
theorem :: ORDINAL6:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "b"))) "iff" (Bool (Set (Var "b"))  ($#r2_hidden :::"nin"::: )  (Set (Var "a")))  ")" )) ; 
 
theorem :: ORDINAL6:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "a"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "b")))) "iff" (Bool  "("  (Bool (Set (Var "b"))  ($#r1_tarski :::"c="::: )  (Set (Var "x"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))  ")" )  ")" ))) ; 
 registrationlet "a", "b" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "a"  ($#k4_xboole_0 :::"\"::: )  "b") ->   ($#v1_ordinal6 :::"ordinal-membered"::: )   ; 
end; 
theorem :: ORDINAL6:6 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X"))) "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "Y"))))) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Var "y"))) "iff" (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y"))))  ")" )))) ; 
 
theorem :: ORDINAL6:7 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X"))) "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "Y"))))) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "y"))) "iff" (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y"))))  ")" )))) ; 
 
theorem :: ORDINAL6:8 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Var "y")))) ; 
 
theorem :: ORDINAL6:9 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"T-Sequence":::) "holds"  (Bool (Set (Var "f1"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f1"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "f2"))))) ; 
 
theorem :: ORDINAL6:10 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"T-Sequence":::) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f1")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f2")) ")" )))) ; 
 
theorem :: ORDINAL6:11 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "b"))) "iff" (Bool (Set   ($#k3_ordinal5 :::"epsilon_"::: )  (Set (Var "a")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k3_ordinal5 :::"epsilon_"::: )  (Set (Var "b"))))  ")" )) ; 
 
theorem :: ORDINAL6:12 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b"))) "iff" (Bool (Set   ($#k3_ordinal5 :::"epsilon_"::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_ordinal5 :::"epsilon_"::: )  (Set (Var "b"))))  ")" )) ; 
 registrationlet "X" be   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_tarski :::"union"::: )  "X") ->   ($#v3_ordinal1 :::"ordinal"::: )   ; 
end; registrationlet "f" be   ($#v1_ordinal2 :::"Ordinal-yielding"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set   ($#k10_xtuple_0 :::"rng"::: )  "f") ->   ($#v1_ordinal6 :::"ordinal-membered"::: )   ; 
end; registrationlet "a" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k4_relat_1 :::"id"::: )  "a") ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_ordinal2 :::"Ordinal-yielding"::: )   ; 
end; registrationlet "a" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k4_relat_1 :::"id"::: )  "a") ->   ($#v2_ordinal2 :::"increasing"::: )    for  ($#m1_hidden :::"Ordinal-Sequence":::); 
end; registrationlet "a" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k4_relat_1 :::"id"::: )  "a") ->   ($#v3_ordinal2 :::"continuous"::: )    for  ($#m1_hidden :::"Ordinal-Sequence":::); 
end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_ordinal2 :::"Ordinal-yielding"::: )     ($#v2_ordinal2 :::"increasing"::: )     ($#v3_ordinal2 :::"continuous"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "f" be   ($#m1_hidden :::"T-Sequence":::); attr "f" is  :::"normal":::  means :: ORDINAL6:def 2 (Bool "f" "is"   ($#v2_ordinal2 :::"increasing"::: )     ($#v3_ordinal2 :::"continuous"::: )    ($#m1_hidden :::"Ordinal-Sequence":::)); end; 




:: deftheorem    defines :::"normal"::: ORDINAL6:def 2 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"T-Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_ordinal6 :::"normal"::: )  ) "iff" (Bool (Set (Var "f")) "is"   ($#v2_ordinal2 :::"increasing"::: )     ($#v3_ordinal2 :::"continuous"::: )    ($#m1_hidden :::"Ordinal-Sequence":::))  ")" )); 
 definitionlet "f" be   ($#m1_hidden :::"Ordinal-Sequence":::); redefine attr "f" is  :::"normal":::  means :: ORDINAL6:def 3 (Bool  "("  (Bool "f" "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool "f" "is"   ($#v3_ordinal2 :::"continuous"::: )  )  ")" ); end; 




:: deftheorem    defines :::"normal"::: ORDINAL6:def 3 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_ordinal6 :::"normal"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set (Var "f")) "is"   ($#v3_ordinal2 :::"continuous"::: )  )  ")" )  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v2_ordinal6 :::"normal"::: )    ->   ($#v1_ordinal2 :::"Ordinal-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_ordinal2 :::"Ordinal-yielding"::: )     ($#v2_ordinal6 :::"normal"::: )    ->   ($#v2_ordinal2 :::"increasing"::: )     ($#v3_ordinal2 :::"continuous"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_ordinal2 :::"Ordinal-yielding"::: )     ($#v2_ordinal2 :::"increasing"::: )     ($#v3_ordinal2 :::"continuous"::: )    ->   ($#v2_ordinal6 :::"normal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_ordinal6 :::"normal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: ORDINAL6:13 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_ordinal5 :::"non-decreasing"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "a"))) "is"   ($#v2_ordinal5 :::"non-decreasing"::: )  ))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"ord-type"::: "X" ->   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   equals :: ORDINAL6:def 4 (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k2_ordinal1 :::"On"::: )  "X" ")" ) ")" )); end; 





:: deftheorem    defines :::"ord-type"::: ORDINAL6:def 4 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_ordinal6 :::"ord-type"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")) ")" ) ")" )))); 
 definitionlet "X" be   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )  ; redefine func  :::"ord-type"::: "X" equals :: ORDINAL6:def 5 (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  "X" ")" )); end; 





:: deftheorem    defines :::"ord-type"::: ORDINAL6:def 5 :  (Bool  "for" (Set (Var "X")) "being"   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_ordinal6 :::"ord-type"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_wellord2 :::"order_type_of"::: )  (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set (Var "X")) ")" )))); 
 registrationlet "X" be   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_wellord2 :::"RelIncl"::: )  "X") ->   ($#v2_wellord1 :::"well-ordering"::: )   ; 
end; registrationlet "E" be   ($#v1_xboole_0 :::"empty"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_ordinal1 :::"On"::: )  "E") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; registrationlet "E" be   ($#v1_xboole_0 :::"empty"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_wellord2 :::"order_type_of"::: )  "E") ->   ($#v1_xboole_0 :::"empty"::: )   ; 
end; 
theorem :: ORDINAL6:14 (Bool (Set   ($#k1_ordinal6 :::"ord-type"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) ; 
 
theorem :: ORDINAL6:15 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_ordinal6 :::"ord-type"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: ORDINAL6:16 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k1_ordinal6 :::"ord-type"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Num 2))) ; 
 
theorem :: ORDINAL6:17 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_ordinal6 :::"ord-type"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a")))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"numbering"::: "X" ->   ($#m1_hidden :::"Ordinal-Sequence":::) equals :: ORDINAL6:def 6 (Set   ($#k3_wellord1 :::"canonical_isomorphism_of"::: )   "(" (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k1_ordinal6 :::"ord-type"::: )  "X" ")" ) ")" ) "," (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k2_ordinal1 :::"On"::: )  "X" ")" ) ")" ) ")" ); end; 





:: deftheorem    defines :::"numbering"::: ORDINAL6:def 6 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_wellord1 :::"canonical_isomorphism_of"::: )   "(" (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k1_ordinal6 :::"ord-type"::: )  (Set (Var "X")) ")" ) ")" ) "," (Set  "("  ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")) ")" ) ")" ) ")" ))); 
 
theorem :: ORDINAL6:18 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal6 :::"ord-type"::: )  (Set (Var "X")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "X"))))  ")" )) ; 
 
theorem :: ORDINAL6:19 (Bool  "for" (Set (Var "X")) "being"   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "X")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 
theorem :: ORDINAL6:20 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "X")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set  "("  ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")) ")" )))) ; 
 
theorem :: ORDINAL6:21 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "X")))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k1_ordinal6 :::"ord-type"::: )  (Set (Var "X")) ")" )) "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set  "("  ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")) ")" )))) ; 
 



theorem :: ORDINAL6:22 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "X")))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Var "y"))) "iff" (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y"))))  ")" ))) ; 
 
theorem :: ORDINAL6:23 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "X")))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "y"))) "iff" (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y"))))  ")" ))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k2_ordinal6 :::"numbering"::: )  "X") ->   ($#v2_ordinal2 :::"increasing"::: )   ; 
end; registrationlet "X", "Y" be   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set "X"  ($#k2_xboole_0 :::"\/"::: )  "Y") ->   ($#v1_ordinal6 :::"ordinal-membered"::: )   ; 
end; registrationlet "X" be   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )  ; let "Y" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "X"  ($#k4_xboole_0 :::"\"::: )  "Y") ->   ($#v1_ordinal6 :::"ordinal-membered"::: )   ; 
end; 
theorem :: ORDINAL6:24 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "y")))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "X")) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  "("  ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "Y")) ")" ))  ($#r3_wellord1 :::"is_isomorphism_of"::: )  (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set  "(" (Set  "("  ($#k1_ordinal6 :::"ord-type"::: )  (Set (Var "X")) ")" )  ($#k10_ordinal2 :::"+^"::: )  (Set  "("  ($#k1_ordinal6 :::"ord-type"::: )  (Set (Var "Y")) ")" ) ")" )) "," (Set   ($#k1_wellord2 :::"RelIncl"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: ORDINAL6:25 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "y")))  ")" )) "holds"  (Bool (Set   ($#k2_ordinal6 :::"numbering"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "X")) ")" )  ($#k1_ordinal4 :::"^"::: )  (Set  "("  ($#k2_ordinal6 :::"numbering"::: )  (Set (Var "Y")) ")" )))) ; 
 
theorem :: ORDINAL6:26 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"   ($#v1_ordinal6 :::"ordinal-membered"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "y")))  ")" )) "holds"  (Bool (Set   ($#k1_ordinal6 :::"ord-type"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_ordinal6 :::"ord-type"::: )  (Set (Var "X")) ")" )  ($#k10_ordinal2 :::"+^"::: )  (Set  "("  ($#k1_ordinal6 :::"ord-type"::: )  (Set (Var "Y")) ")" )))) ; 
 begin  
theorem :: ORDINAL6:27 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))))) ; 
 definitionlet "f" be   ($#m1_hidden :::"Ordinal-Sequence":::); func  :::"criticals"::: "f" ->   ($#m1_hidden :::"Ordinal-Sequence":::) equals :: ORDINAL6:def 7 (Set   ($#k2_ordinal6 :::"numbering"::: )   "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  "f") : (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  "f")  "}"  ); end; 





:: deftheorem    defines :::"criticals"::: ORDINAL6:def 7 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"  (Bool (Set   ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal6 :::"numbering"::: )   "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))) : (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))  "}"  ))); 
 
theorem :: ORDINAL6:28 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"  (Bool (Set   ($#k2_ordinal1 :::"On"::: )   "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))) : (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))  "}"  )  ($#r1_hidden :::"="::: )   "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))) : (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))  "}"  )) ; 
 
theorem :: ORDINAL6:29 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f"))))) ; 
 
theorem :: ORDINAL6:30 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"   (Bool  "("  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))) : (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))  "}"  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f"))))  ")" )) ; 
 registrationlet "f" be   ($#m1_hidden :::"Ordinal-Sequence":::); 
cluster (Set   ($#k3_ordinal6 :::"criticals"::: )  "f") ->   ($#v2_ordinal2 :::"increasing"::: )   ; 
end; 
theorem :: ORDINAL6:31 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))) ; 
 
theorem :: ORDINAL6:32 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) ; 
 
theorem :: ORDINAL6:33 (Bool  "for" (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "b"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))) "holds"  (Bool  "ex" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))  ")" )))) ; 
 
theorem :: ORDINAL6:34 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "b"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f"))) & (Bool (Set (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: ORDINAL6:35 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "b"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f"))) & (Bool (Set (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "a")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "b"))))) ; 
 
theorem :: ORDINAL6:36 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_ordinal6 :::"normal"::: )  ) & (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Var "y"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "y"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))  ")" ))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "X")) ")" ))))) ; 
 
theorem :: ORDINAL6:37 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_ordinal6 :::"normal"::: )  ) & (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Bool  "not" (Set (Var "X")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "x"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set (Var "X")) ")" ))))) ; 
 
theorem :: ORDINAL6:38 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "l")) "being"   ($#v4_ordinal1 :::"limit_ordinal"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" ))) & (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f"))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "l")))) "holds"  (Bool (Set (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))  ")" )) "holds"  (Bool (Set (Var "l"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )))))) ; 
 
theorem :: ORDINAL6:39 (Bool  "for" (Set (Var "l")) "being"   ($#v4_ordinal1 :::"limit_ordinal"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_ordinal6 :::"normal"::: )  ) & (Bool (Set (Var "l"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "l")) ")" ))))) ; 
 registrationlet "f" be   ($#v2_ordinal6 :::"normal"::: )    ($#m1_hidden :::"Ordinal-Sequence":::); 
cluster (Set   ($#k3_ordinal6 :::"criticals"::: )  "f") ->   ($#v3_ordinal2 :::"continuous"::: )   ; 
end; 
theorem :: ORDINAL6:40 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_tarski :::"c="::: )  (Set (Var "f2")))) "holds"  (Bool (Set   ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f1")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f2"))))) ; 
 begin  



registrationlet "U" be   ($#m1_hidden :::"Universe":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k2_ordinal1 :::"On"::: )  "U")  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k2_ordinal1 :::"On"::: )  "U")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  bbbadV1_PARTFUN1((Set   ($#k2_ordinal1 :::"On"::: )  "U")) bbbadV1_FUNCT_2((Set   ($#k2_ordinal1 :::"On"::: )  "U") "," (Set   ($#k2_ordinal1 :::"On"::: )  "U"))   ($#v1_ordinal2 :::"Ordinal-yielding"::: )     ($#v2_ordinal6 :::"normal"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k2_ordinal1 :::"On"::: )  "U" ")" ) "," (Set  "("  ($#k2_ordinal1 :::"On"::: )  "U" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "U" be   ($#m1_hidden :::"Universe":::); let "a" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; mode Ordinal-Sequence of "a" "," "U" is   ($#m1_subset_1 :::"Function":::) "of" "a" "," (Set  "("  ($#k2_ordinal1 :::"On"::: )  "U" ")" ); end; registrationlet "U" be   ($#m1_hidden :::"Universe":::); let "a" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2("a" "," (Set   ($#k2_ordinal1 :::"On"::: )  "U"))  ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_ordinal2 :::"Ordinal-yielding"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) "a" "," (Set  "("  ($#k2_ordinal1 :::"On"::: )  "U" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "U" be   ($#m1_hidden :::"Universe":::); let "a" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; let "f" be   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Const "a")) "," (Set (Const "U")); let "x" be    ($#m1_hidden :::"set"::: )  ; :: original: :::"."::: redefine func "f" :::"."::: "x" ->   ($#m1_subset_1 :::"Ordinal":::) "of" "U"; end; 
theorem :: ORDINAL6:41 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "a")) "," (Set (Var "U")) "holds"  (Bool (Set   ($#k3_card_3 :::"Union"::: )  (Set (Var "f")))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))))) ; 
 
theorem :: ORDINAL6:42 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "a")) "," (Set (Var "U")) "holds"  (Bool (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "f")))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))))) ; 
 scheme  :: ORDINAL6:sch 1 CriticalNumber2{ F1() ->   ($#m1_hidden :::"Universe":::), F2() ->   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ), F3() ->   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set  ($#k4_ordinal1 :::"omega"::: ) ) "," (Set F1 "("  ")" ), F4(  ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::) } : 
(Bool  "("  (Bool (Set F2 "("  ")" )  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set F3 "("  ")" ))) & (Bool (Set F4 "(" (Set  "("  ($#k3_card_3 :::"Union"::: )  (Set F3 "("  ")" ) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set F3 "("  ")" ))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set F2 "("  ")" )  ($#r1_ordinal1 :::"c="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set F4 "(" (Set (Var "b")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k3_card_3 :::"Union"::: )  (Set F3 "("  ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "b")))  ")" )  ")" )
 provided
(Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool (Set F4 "(" (Set (Var "a")) ")" )  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool (Set F4 "(" (Set (Var "a")) ")" )  ($#r2_hidden :::"in"::: )  (Set F4 "(" (Set (Var "b")) ")" )))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "a")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool  "for" (Set (Var "phi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "phi")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Set (Var "phi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "b")) ")" ))  ")" )) "holds"  (Bool (Set F4 "(" (Set (Var "a")) ")" )  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "phi")))))
 and  
(Bool (Set (Set F3 "("  ")" )  ($#k4_ordinal6 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k4_ordinal6 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set  "(" (Set F3 "("  ")" )  ($#k4_ordinal6 :::"."::: )  (Set (Var "a")) ")" ) ")" )))
 proof 


end; scheme  :: ORDINAL6:sch 2 CriticalNumber3{ F1() ->   ($#m1_hidden :::"Universe":::), F2() ->   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ), F3(  ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::) } : 
(Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set F2 "("  ")" )  ($#r2_hidden :::"in"::: )  (Set (Var "a"))) & (Bool (Set F3 "(" (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")" ))
 provided
(Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool (Set F3 "(" (Set (Var "a")) ")" )  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )))
 and  
(Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool (Set F3 "(" (Set (Var "a")) ")" )  ($#r2_hidden :::"in"::: )  (Set F3 "(" (Set (Var "b")) ")" )))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Bool  "not" (Set (Var "a")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "a")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool  "for" (Set (Var "phi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "phi")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))) "holds"  (Bool (Set (Set (Var "phi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "b")) ")" ))  ")" )) "holds"  (Bool (Set F3 "(" (Set (Var "a")) ")" )  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "phi")))))
 proof 


end; 




theorem :: ORDINAL6:43 (Bool  "for" (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "phi")) "being"   ($#v2_ordinal6 :::"normal"::: )    ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool  "ex" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "a"))) & (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "phi")))  ")" ))))) ; 
 
theorem :: ORDINAL6:44 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "F")) "being"   ($#v2_ordinal6 :::"normal"::: )    ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set   ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "F"))) "is"   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W"))))) ; 
 
theorem :: ORDINAL6:45 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_ordinal6 :::"normal"::: )  )) "holds"  (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set  "("  ($#k3_ordinal6 :::"criticals"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))))) ; 
 begin  definitionlet "U" be   ($#m1_hidden :::"Universe":::); let "a", "b" be   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Const "U")); :: original: :::"exp"::: redefine func  :::"exp":::  "(" "a" "," "b" ")"  ->   ($#m1_subset_1 :::"Ordinal":::) "of" "U"; end; definitionlet "U" be   ($#m1_hidden :::"Universe":::); let "a" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; assume 
(Bool (Set (Const "a"))  ($#r2_hidden :::"in"::: )  (Set (Const "U")))
 ; func "U" :::"exp"::: "a" ->   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" "U" means :: ORDINAL6:def 8 (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" "U" "holds"  (Bool (Set it  ($#k4_ordinal6 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" "a" "," (Set (Var "b")) ")" ))); end; 







:: deftheorem    defines :::"exp"::: ORDINAL6:def 8 :  (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "U")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "U"))  ($#k6_ordinal6 :::"exp"::: )  (Set (Var "a")))) "iff" (Bool  "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "U")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k4_ordinal6 :::"."::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )))  ")" )))); 
 registration
cluster (Set   ($#k4_ordinal1 :::"omega"::: )  ) ->  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )  ; 
end; registrationlet "U" be   ($#m1_hidden :::"Universe":::); 
cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )    ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_ordinal6 :::"ordinal-membered"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "U"; 
end; registration
cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )    ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_ordinal6 :::"ordinal-membered"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "U" be   ($#m1_hidden :::"Universe":::); let "a" be  ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"trivial"::: )   )   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Const "U")); 
cluster (Set "U"  ($#k6_ordinal6 :::"exp"::: )  "a") ->   ($#v2_ordinal6 :::"normal"::: )   ; 
end; definitionlet "g" be   ($#m1_hidden :::"Function":::); attr "g" is  :::"Ordinal-Sequence-valued":::  means :: ORDINAL6:def 9 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  "g"))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Ordinal-Sequence":::))); end; 




:: deftheorem    defines :::"Ordinal-Sequence-valued"::: ORDINAL6:def 9 :  (Bool  "for" (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "g")) "is"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Ordinal-Sequence":::)))  ")" )); 
 registrationlet "f" be   ($#m1_hidden :::"Ordinal-Sequence":::); 
cluster (Set  ($#k3_afinsq_1 :::"<%"::: ) "f" ($#k3_afinsq_1 :::"%>"::: ) ) ->   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )   ; 
end; definitionlet "f" be   ($#m1_hidden :::"Function":::); attr "f" is  :::"with_the_same_dom":::  means :: ORDINAL6:def 10 (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  "f") "is"   ($#v2_card_3 :::"with_common_domain"::: )  ); end; 




:: deftheorem    defines :::"with_the_same_dom"::: ORDINAL6:def 10 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v4_ordinal6 :::"with_the_same_dom"::: )  ) "iff" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f"))) "is"   ($#v2_card_3 :::"with_common_domain"::: )  )  ")" )); 
 registrationlet "f" be   ($#m1_hidden :::"Function":::); 
cluster (Set  ($#k1_tarski :::"{"::: ) "f" ($#k1_tarski :::"}"::: ) ) ->   ($#v2_card_3 :::"with_common_domain"::: )   ; 
end; registrationlet "f" be   ($#m1_hidden :::"Function":::); 
cluster (Set  ($#k3_afinsq_1 :::"<%"::: ) "f" ($#k3_afinsq_1 :::"%>"::: ) ) ->   ($#v4_ordinal6 :::"with_the_same_dom"::: )   ; 
end; registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )     ($#v4_ordinal6 :::"with_the_same_dom"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "g" be   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"Function":::); let "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "g"  ($#k1_funct_1 :::"."::: )  "x") ->   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )   ; 
end; registrationlet "g" be   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"Function":::); let "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "g"  ($#k1_funct_1 :::"."::: )  "x") ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_ordinal2 :::"Ordinal-yielding"::: )   ; 
end; registrationlet "g" be   ($#m1_hidden :::"T-Sequence":::); let "a" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "g"  ($#k5_relat_1 :::"|"::: )  "a") ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )   ; 
end; registrationlet "g" be   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"Function":::); let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "g"  ($#k5_relat_1 :::"|"::: )  "X") ->   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )   ; 
end; registrationlet "a", "b" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2("a" "," "b")  ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_ordinal2 :::"Ordinal-yielding"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) "a" "," "b" ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "g" be   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::); func  :::"criticals"::: "g" ->   ($#m1_hidden :::"Ordinal-Sequence":::) equals :: ORDINAL6:def 11 (Set   ($#k2_ordinal6 :::"numbering"::: )   "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" "g"  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )) : (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" "g"  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  "g"))) "holds"  (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))  ")" )  ")" )  "}"  ); end; 





:: deftheorem    defines :::"criticals"::: ORDINAL6:def 11 :  (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::) "holds"  (Bool (Set   ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal6 :::"numbering"::: )   "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )) : (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))  ")" )  ")" )  "}"  ))); 
 



theorem :: ORDINAL6:46 (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::) "holds"  (Bool  "{"  (Set (Var "a")) where a "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" )) : (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))  ")" )  ")" )  "}"   "is"   ($#v1_ordinal6 :::"ordinal-membered"::: )  )) ; 
 
theorem :: ORDINAL6:47 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))))) ; 
 
theorem :: ORDINAL6:48 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" )))) "holds"  (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))) ; 
 
theorem :: ORDINAL6:49 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g"))))) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" ))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))))) ; 
 
theorem :: ORDINAL6:50 (Bool  "for" (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "b"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c"))))  ")" )) "holds"  (Bool  "ex" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" ))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))  ")" )))) ; 
 
theorem :: ORDINAL6:51 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "l")) "being"   ($#v4_ordinal1 :::"limit_ordinal"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "l"))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" ))) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Var "f")))  ")" ) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "l")))) "holds"  (Bool (Set (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Var "a")))  ")" )) "holds"  (Bool (Set (Var "l"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" )))))) ; 
 
theorem :: ORDINAL6:52 (Bool  "for" (Set (Var "l")) "being"   ($#v4_ordinal1 :::"limit_ordinal"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))) "is"   ($#v2_ordinal6 :::"normal"::: )  )  ")" ) & (Bool (Set (Var "l"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" )))) "holds"  (Bool (Set (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "l")) ")" ))))) ; 
 
theorem :: ORDINAL6:53 (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))) "is"   ($#v2_ordinal6 :::"normal"::: )  )  ")" )) "holds"  (Bool (Set   ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g"))) "is"   ($#v3_ordinal2 :::"continuous"::: )  )) ; 
 
theorem :: ORDINAL6:54 (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))) "is"   ($#v2_ordinal6 :::"normal"::: )  )  ")" )) "holds"  (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" ))) & (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set  "("  ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))))) ; 
 
theorem :: ORDINAL6:55 (Bool  "for" (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g1")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g2")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g1")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g1"))))) "holds"  (Bool (Set (Set (Var "g1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "g2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))))  ")" )) "holds"  (Bool (Set   ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g1")))  ($#r1_tarski :::"c="::: )  (Set   ($#k7_ordinal6 :::"criticals"::: )  (Set (Var "g2"))))) ; 
 definitionlet "g" be   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::); func  :::"lims"::: "g" ->   ($#m1_hidden :::"Ordinal-Sequence":::) means :: ORDINAL6:def 12 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" "g"  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "(" (Set  "(" "g"  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")) ")" ) where b "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  "g") : (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "g"))  "}"  ))  ")" )  ")" ); end; 





:: deftheorem    defines :::"lims"::: ORDINAL6:def 12 :  (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_ordinal6 :::"lims"::: )  (Set (Var "g")))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "(" (Set  "(" (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")) ")" ) where b "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))) : (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))  "}"  ))  ")" )  ")" )  ")" ))); 
 
theorem :: ORDINAL6:56 (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "g")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))) "is"   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "U")))  ")" )) "holds"  (Bool (Set   ($#k8_ordinal6 :::"lims"::: )  (Set (Var "g"))) "is"   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "U"))))) ; 
 begin  definitionlet "x" be    ($#m1_hidden :::"set"::: )  ; func  :::"OS@"::: "x" ->   ($#m1_hidden :::"Ordinal-Sequence":::) equals :: ORDINAL6:def 13 "x" if (Bool "x" "is"   ($#m1_hidden :::"Ordinal-Sequence":::))  otherwise  "the"   ($#m1_hidden :::"Ordinal-Sequence":::); func  :::"OSV@"::: "x" ->   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::) equals :: ORDINAL6:def 14 "x" if (Bool "x" "is"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::))  otherwise  "the"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::); end; 










:: deftheorem    defines :::"OS@"::: ORDINAL6:def 13 :  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Ordinal-Sequence":::))) "implies" (Bool (Set   ($#k9_ordinal6 :::"OS@"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")"  &  "("  (Bool (Bool (Set (Var "x")) "is" (Bool  "not"   ($#m1_hidden :::"Ordinal-Sequence":::)))) "implies" (Bool (Set   ($#k9_ordinal6 :::"OS@"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )   "the"   ($#m1_hidden :::"Ordinal-Sequence":::))  ")"   ")" )); 
 
:: deftheorem    defines :::"OSV@"::: ORDINAL6:def 14 :  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x")) "is"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::))) "implies" (Bool (Set   ($#k10_ordinal6 :::"OSV@"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")"  &  "("  (Bool (Bool (Set (Var "x")) "is" (Bool  "not"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::)))) "implies" (Bool (Set   ($#k10_ordinal6 :::"OSV@"::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )   "the"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::))  ")"   ")" )); 
 definitionlet "U" be   ($#m1_hidden :::"Universe":::); func "U" :::"-Veblen":::  ->   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::) means :: ORDINAL6:def 15 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal1 :::"On"::: )  "U")) & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set "U"  ($#k6_ordinal6 :::"exp"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "b")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_ordinal1 :::"On"::: )  "U"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_ordinal6 :::"criticals"::: )  (Set  "(" it  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "l")) "being"   ($#v4_ordinal1 :::"limit_ordinal"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_ordinal1 :::"On"::: )  "U"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_ordinal6 :::"criticals"::: )  (Set  "(" it  ($#k5_relat_1 :::"|"::: )  (Set (Var "l")) ")" )))  ")" )  ")" ); end; 





:: deftheorem    defines :::"-Veblen"::: ORDINAL6:def 15 :  (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v3_ordinal6 :::"Ordinal-Sequence-valued"::: )    ($#m1_hidden :::"T-Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  )) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "U")))) & (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "U"))  ($#k6_ordinal6 :::"exp"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ))) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "b")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "U"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "b")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_ordinal6 :::"criticals"::: )  (Set  "(" (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "l")) "being"   ($#v4_ordinal1 :::"limit_ordinal"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "U"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "l")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_ordinal6 :::"criticals"::: )  (Set  "(" (Set (Var "b2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "l")) ")" )))  ")" )  ")" )  ")" ))); 
 registration
cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_classes1 :::"subset-closed"::: )     ($#v2_classes1 :::"Tarski"::: )     ($#v4_card_3 :::"uncountable"::: )     ($#v1_classes2 :::"universal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: ORDINAL6:57 (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::) "holds"   (Bool  "("  (Bool (Set (Var "U")) "is"   ($#v4_card_3 :::"uncountable"::: )  ) "iff" (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "U")))  ")" )) ; 
 
theorem :: ORDINAL6:58 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" )))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))))) ; 
 
theorem :: ORDINAL6:59 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "l")) "being"   ($#v4_ordinal1 :::"limit_ordinal"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "l")))) "holds"  (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c"))))  ")" )) "holds"  (Bool (Set (Var "a"))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set   ($#k8_ordinal6 :::"lims"::: )  (Set  "(" (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "l")) ")" )))))) ; 
 
theorem :: ORDINAL6:60 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "b"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" ))) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c"))) "is"   ($#v2_ordinal6 :::"normal"::: )  )  ")" )) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set  "(" (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))))) ; 
 
theorem :: ORDINAL6:61 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "l")) "being"   ($#v4_ordinal1 :::"limit_ordinal"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "l"))) & (Bool  "("   "for" (Set (Var "c")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "l")))) "holds"  (Bool (Set (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c"))) "is"   ($#v2_ordinal6 :::"normal"::: )    ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "U")))  ")" )) "holds"  (Bool (Set (Set  "("  ($#k8_ordinal6 :::"lims"::: )  (Set  "(" (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "l")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_abian :::"is_a_fixpoint_of"::: )  (Set (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b"))))))) ; 
 
theorem :: ORDINAL6:62 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool (Set (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))) "is"   ($#v2_ordinal6 :::"normal"::: )    ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "U"))))) ; 
 
theorem :: ORDINAL6:63 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "U")) "," (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "U"))  ($#r1_tarski :::"c="::: )  (Set (Var "W"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool (Set (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Set  "(" (Set (Var "W"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))))) ; 
 
theorem :: ORDINAL6:64 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "U")) "," (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "W"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))))) ; 
 
theorem :: ORDINAL6:65 (Bool  "for" (Set (Var "l")) "being"   ($#v4_ordinal1 :::"limit_ordinal"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set (Var "l"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "l")))) "holds"  (Bool (Set (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a"))) "is"   ($#v2_ordinal6 :::"normal"::: )    ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "U")))  ")" )) "holds"  (Bool (Set   ($#k8_ordinal6 :::"lims"::: )  (Set  "(" (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "l")) ")" )) "is"   ($#v3_ordinal2 :::"continuous"::: )     ($#v2_ordinal5 :::"non-decreasing"::: )    ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "U"))))) ; 
 registrationlet "a" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set  "(" "a"  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ) ")" )) ->   ($#v4_card_3 :::"uncountable"::: )   ; 
end; definitionlet "a", "b" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; func "a" :::"-Veblen"::: "b" ->   ($#m1_hidden :::"Ordinal":::) equals :: ORDINAL6:def 16 (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set  "(" (Set  "(" "a"  ($#k2_xboole_0 :::"\/"::: )  "b" ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ) ")" ) ")" )  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  "a" ")" )  ($#k1_funct_1 :::"."::: )  "b"); end; 






:: deftheorem    defines :::"-Veblen"::: ORDINAL6:def 16 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "b")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ) ")" ) ")" )  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b"))))); 
 definitionlet "n" be   ($#m1_hidden :::"Nat":::); let "b" be   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; :: original: :::"-Veblen"::: redefine func "n" :::"-Veblen"::: "b" ->   ($#m1_hidden :::"Ordinal":::) equals :: ORDINAL6:def 17 (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set  "(" "b"  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ) ")" ) ")" )  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  "n" ")" )  ($#k1_funct_1 :::"."::: )  "b"); end; 






:: deftheorem    defines :::"-Veblen"::: ORDINAL6:def 17 :  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "n"))  ($#k13_ordinal6 :::"-Veblen"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k1_classes1 :::"Tarski-Class"::: )  (Set  "(" (Set (Var "b"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ) ")" ) ")" )  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")))))); 
 
theorem :: ORDINAL6:66 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_classes1 :::"Tarski-Class"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "b")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "c")) ")" )))) ; 
 
theorem :: ORDINAL6:67 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "U")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "U"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "U")))) "holds"  (Bool (Set (Set (Var "b"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "b")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))))) ; 
 
theorem :: ORDINAL6:68 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k13_ordinal6 :::"-Veblen"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set  ($#k4_ordinal1 :::"omega"::: ) ) "," (Set (Var "a")) ")" ))) ; 
 
theorem :: ORDINAL6:69 (Bool  "for" (Set (Var "b")) "," (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "b"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set  "(" (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "b")) ")" )  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "b")) ")" )  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "a"))))) ; 
 
theorem :: ORDINAL6:70 (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "c")))) "holds"  (Bool (Set (Set (Var "b"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set  "(" (Set (Var "c"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "a"))))) ; 
 
theorem :: ORDINAL6:71 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "b"))) "iff" (Bool (Set (Set (Var "c"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "a")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "c"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "b"))))  ")" )) ; 
 
theorem :: ORDINAL6:72 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b"))) "iff" (Bool (Set (Set (Var "c"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "a")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "c"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "b"))))  ")" )) ; 
 
theorem :: ORDINAL6:73 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "a"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "b")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "c"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "d")))) "iff" (Bool  "("  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Var "d")))  ")" ) "or" (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "c"))) & (Bool (Set (Var "b"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "c"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "d"))))  ")" ) "or" (Bool  "("  (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "a"))  ($#k12_ordinal6 :::"-Veblen"::: )  (Set (Var "b")))  ($#r2_hidden :::"in"::: )  (Set (Var "d")))  ")" )  ")" )  ")" )) ; 
 begin  



theorem :: ORDINAL6:74 (Bool  "for" (Set (Var "U")) "being"   ($#v4_card_3 :::"uncountable"::: )    ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set (Set  "(" (Set (Var "U"))  ($#k11_ordinal6 :::"-Veblen"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k3_ordinal6 :::"criticals"::: )  (Set  "(" (Set (Var "U"))  ($#k6_ordinal6 :::"exp"::: )  (Set  ($#k4_ordinal1 :::"omega"::: ) ) ")" )))) ; 
 
theorem :: ORDINAL6:75 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k13_ordinal6 :::"-Veblen"::: )  (Set (Var "a"))) "is"   ($#v4_ordinal5 :::"epsilon"::: )  )) ; 
 
theorem :: ORDINAL6:76 (Bool  "for" (Set (Var "e")) "being"   ($#v4_ordinal5 :::"epsilon"::: )    ($#m1_hidden :::"Ordinal":::) (Bool  "ex" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "st" (Bool (Set (Var "e"))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k13_ordinal6 :::"-Veblen"::: )  (Set (Var "a")))))) ; 
 
theorem :: ORDINAL6:77 (Bool  "for" (Set (Var "a")) "being"   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Num 1)  ($#k13_ordinal6 :::"-Veblen"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_ordinal5 :::"epsilon_"::: )  (Set (Var "a"))))) ;