:: ORDINAL1  semantic presentation begin  













theorem :: ORDINAL1:1 canceled; 
 
theorem :: ORDINAL1:2 canceled; 
 
theorem :: ORDINAL1:3 canceled; 
 
theorem :: ORDINAL1:4 canceled; 
 
theorem :: ORDINAL1:5 (Bool  "for" (Set (Var "Y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "Y"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "not" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y"))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"succ"::: "X" ->    ($#m1_hidden :::"set"::: )   equals :: ORDINAL1:def 1 (Set "X"  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) "X" ($#k1_tarski :::"}"::: ) )); end; 





:: deftheorem    defines :::"succ"::: ORDINAL1:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) )))); 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_ordinal1 :::"succ"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: ORDINAL1:6 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "X"))))) ; 
 
theorem :: ORDINAL1:7 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "Y"))))) "holds"  (Bool (Set (Var "X"))  ($#r1_hidden :::"="::: )  (Set (Var "Y")))) ; 
 
theorem :: ORDINAL1:8 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "X")))  ")" )  ")" )) ; 
 
theorem :: ORDINAL1:9 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds" (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "X"))))) ; 
 










definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; attr "X" is  :::"epsilon-transitive":::  means :: ORDINAL1:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X")) "holds"  (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  "X")); attr "X" is  :::"epsilon-connected":::  means :: ORDINAL1:def 3 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "y")))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "x")))); end; 








:: deftheorem    defines :::"epsilon-transitive"::: ORDINAL1:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) "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"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))))  ")" )); 
 
:: deftheorem    defines :::"epsilon-connected"::: ORDINAL1:def 3 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v2_ordinal1 :::"epsilon-connected"::: )  ) "iff" (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"))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "y")))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "x"))))  ")" )); 
 definitionlet "IT" be    ($#m1_hidden :::"set"::: )  ; attr "IT" is  :::"ordinal":::  means :: ORDINAL1:def 4 (Bool  "("  (Bool "IT" "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) & (Bool "IT" "is"   ($#v2_ordinal1 :::"epsilon-connected"::: )  )  ")" ); end; 




:: deftheorem    defines :::"ordinal"::: ORDINAL1:def 4 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_ordinal1 :::"ordinal"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_ordinal1 :::"epsilon-transitive"::: )  ) & (Bool (Set (Var "IT")) "is"   ($#v2_ordinal1 :::"epsilon-connected"::: )  )  ")" )  ")" )); 
 registration
cluster   ($#v3_ordinal1 :::"ordinal"::: )    ->   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )    for    ($#m1_hidden :::"number"::: )  ; 

cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )    ->   ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_hidden :::"number"::: )  ; 
end; notationsynonym  :::"number":::  for  :::"set"::: ; end; registration
cluster   ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_hidden :::"number"::: )  ; 
end; definitionmode Ordinal is   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_hidden :::"number"::: )  ; end; 






theorem :: ORDINAL1:10 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))))) ; 
 
theorem :: ORDINAL1:11 (Bool  "for" (Set (Var "x")) "being"   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))) ; 
 
theorem :: ORDINAL1:12 (Bool  "for" (Set (Var "A")) "being"   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_tarski :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))))) ; 
 
theorem :: ORDINAL1:13 (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "a")) "is"   ($#m1_hidden :::"Ordinal":::)))) ; 
 
theorem :: ORDINAL1:14 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "holds"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B"))) "or" (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )) ; 
 definitionlet "A", "B" be   ($#m1_hidden :::"Ordinal":::); :: original: :::"c="::: redefine pred "A" :::"c="::: "B" means :: ORDINAL1:def 5 (Bool  "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  "A")) "holds"  (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  "B")); connectedness  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool  "ex" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Bool  "not" (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))))  ")" ))) "holds"  (Bool  "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))))
 ; end; 





:: deftheorem    defines :::"c="::: ORDINAL1:def 5 :  (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  "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))))  ")" )); 
 
theorem :: ORDINAL1:15 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  )) ; 
 
theorem :: ORDINAL1:16 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "holds"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B"))) "or" (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))  ")" )) ; 
 registration
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_hidden :::"number"::: )  ; 
end; 
theorem :: ORDINAL1:17 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Ordinal":::))) "holds"  (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "x"))) "is"   ($#m1_hidden :::"Ordinal":::))) ; 
 
theorem :: ORDINAL1:18 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x")) "is"   ($#v3_ordinal1 :::"ordinal"::: )  )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "x"))) "is"   ($#v3_ordinal1 :::"ordinal"::: )  )) ; 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_hidden :::"number"::: )  ; 
end; registrationlet "A" be   ($#m1_hidden :::"Ordinal":::); 
cluster (Set   ($#k1_ordinal1 :::"succ"::: )  "A") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_ordinal1 :::"ordinal"::: )   ; 

cluster (Set   ($#k3_tarski :::"union"::: )  "A") ->   ($#v3_ordinal1 :::"ordinal"::: )   ; 
end; 
theorem :: ORDINAL1:19 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Ordinal":::)) & (Bool (Set (Var "x"))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))  ")" )  ")" )) "holds"  (Bool (Set (Var "X")) "is"   ($#v3_ordinal1 :::"ordinal"::: )  )) ; 
 
theorem :: ORDINAL1:20 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "X"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool  "ex" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "C"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))  ")" )  ")" )))) ; 
 
theorem :: ORDINAL1:21 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) "iff" (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))  ")" )) ; 
 
theorem :: ORDINAL1:22 (Bool  "for" (Set (Var "A")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))) "iff" (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "C")))  ")" )) ; 
 scheme  :: ORDINAL1:sch 1 OrdinalMin{ P1[  ($#m1_hidden :::"Ordinal":::)] } : 
(Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool P1[(Set (Var "A"))]) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool P1[(Set (Var "B"))])) "holds"  (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))  ")" )  ")" ))
 provided
(Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool P1[(Set (Var "A"))]))
 proof 


end; scheme  :: ORDINAL1:sch 2 TransfiniteInd{ P1[  ($#m1_hidden :::"Ordinal":::)] } : 
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool P1[(Set (Var "A"))]))
 provided
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool P1[(Set (Var "C"))])  ")" )) "holds"  (Bool P1[(Set (Var "A"))]))
 proof 


end; 
theorem :: ORDINAL1:23 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "a")) "is"   ($#m1_hidden :::"Ordinal":::))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))) "is"   ($#v3_ordinal1 :::"ordinal"::: )  )) ; 
 
theorem :: ORDINAL1:24 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "a")) "is"   ($#m1_hidden :::"Ordinal":::))  ")" )) "holds"  (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))))) ; 
 
theorem :: ORDINAL1:25 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "not" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Ordinal":::))  ")" )))) ; 
 
theorem :: ORDINAL1:26 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "not" (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))))) ; 
 
theorem :: ORDINAL1:27 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Bool  "not" (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))  ")" )  ")" ))) ; 
 definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; attr "A" is  :::"limit_ordinal":::  means :: ORDINAL1:def 6 (Bool "A"  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  "A")); end; 




:: deftheorem    defines :::"limit_ordinal"::: ORDINAL1:def 6 :  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) "iff" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set (Var "A"))))  ")" )); 
 
theorem :: ORDINAL1:28 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) "iff" (Bool  "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))))  ")" )) ; 
 
theorem :: ORDINAL1:29 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Bool  "not" (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "iff" (Bool  "ex" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")))))  ")" )) ; 
 



definitionlet "IT" be    ($#m1_hidden :::"set"::: )  ; attr "IT" is  :::"T-Sequence-like":::  means :: ORDINAL1:def 7 (Bool (Set   ($#k9_xtuple_0 :::"proj1"::: )  "IT") "is"   ($#v3_ordinal1 :::"ordinal"::: )  ); end; 




:: deftheorem    defines :::"T-Sequence-like"::: ORDINAL1:def 7 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v5_ordinal1 :::"T-Sequence-like"::: )  ) "iff" (Bool (Set   ($#k9_xtuple_0 :::"proj1"::: )  (Set (Var "IT"))) "is"   ($#v3_ordinal1 :::"ordinal"::: )  )  ")" )); 
 registration
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )    for    ($#m1_hidden :::"number"::: )  ; 
end; definitionmode T-Sequence is   ($#v5_ordinal1 :::"T-Sequence-like"::: )    ($#m1_hidden :::"Function":::); end; registrationlet "Z" be    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "Z"  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )    for    ($#m1_hidden :::"number"::: )  ; 
end; definitionlet "Z" be    ($#m1_hidden :::"set"::: )  ; mode T-Sequence of "Z" is "Z"  ($#v5_relat_1 :::"-valued"::: )    ($#m1_hidden :::"T-Sequence":::); end; 
theorem :: ORDINAL1:30 (Bool  "for" (Set (Var "Z")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"   ($#m1_hidden :::"T-Sequence":::) "of" (Set (Var "Z")))) ; 
 




theorem :: ORDINAL1:31 (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F"))) "is"   ($#m1_hidden :::"Ordinal":::))) "holds"  (Bool (Set (Var "F")) "is"   ($#m1_hidden :::"T-Sequence":::) "of" (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "F"))))) ; 
 registrationlet "L" be   ($#m1_hidden :::"T-Sequence":::); 
cluster (Set   ($#k9_xtuple_0 :::"proj1"::: )  "L") ->   ($#v3_ordinal1 :::"ordinal"::: )   ; 
end; 
theorem :: ORDINAL1:32 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "of" (Set (Var "X")) "holds"  (Bool (Set (Var "L")) "is"   ($#m1_hidden :::"T-Sequence":::) "of" (Set (Var "Y"))))) ; 
 registrationlet "L" be   ($#m1_hidden :::"T-Sequence":::); let "A" be   ($#m1_hidden :::"Ordinal":::); 
cluster (Set "L"  ($#k5_relat_1 :::"|"::: )  "A") -> (Set   ($#k10_xtuple_0 :::"rng"::: )  "L")  ($#v5_relat_1 :::"-valued"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )   ; 
end; 
theorem :: ORDINAL1:33 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "A"))) "is"   ($#m1_hidden :::"T-Sequence":::) "of" (Set (Var "X")))))) ; 
 definitionlet "IT" be    ($#m1_hidden :::"set"::: )  ; attr "IT" is  :::"c=-linear":::  means :: ORDINAL1:def 8 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "IT") & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  "IT")) "holds"  (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  )); end; 




:: deftheorem    defines :::"c=-linear"::: ORDINAL1:def 8 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v6_ordinal1 :::"c=-linear"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT"))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT")))) "holds"  (Bool (Set (Var "x")) "," (Set (Var "y"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  ))  ")" )); 
 
theorem :: ORDINAL1:34 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "a")) "is"   ($#m1_hidden :::"T-Sequence":::))  ")" ) & (Bool (Set (Var "X")) "is"   ($#v6_ordinal1 :::"c=-linear"::: )  )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))) "is"   ($#m1_hidden :::"T-Sequence":::))) ; 
 scheme  :: ORDINAL1:sch 3 TSUniq{ F1() ->   ($#m1_hidden :::"Ordinal":::), F2(  ($#m1_hidden :::"T-Sequence":::)) ->    ($#m1_hidden :::"set"::: )  , F3() ->   ($#m1_hidden :::"T-Sequence":::), F4() ->   ($#m1_hidden :::"T-Sequence":::) } : 
(Bool (Set F3 "("  ")" )  ($#r1_hidden :::"="::: )  (Set F4 "("  ")" ))
 provided
(Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F3 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "L"))  ($#r1_hidden :::"="::: )  (Set (Set F3 "("  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "L")) ")" )))  ")" )  ")" )
 and  
(Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F4 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "L"))  ($#r1_hidden :::"="::: )  (Set (Set F4 "("  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Set F4 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "L")) ")" )))  ")" )  ")" )
 proof 


end; scheme  :: ORDINAL1:sch 4 TSExist{ F1() ->   ($#m1_hidden :::"Ordinal":::), F2(  ($#m1_hidden :::"T-Sequence":::)) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "L1")) "being"   ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "L1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "L1")) ")" )))  ")" )  ")" ))
 proof 


end; scheme  :: ORDINAL1:sch 5 FuncTS{ F1() ->   ($#m1_hidden :::"T-Sequence":::), F2(  ($#m1_hidden :::"Ordinal":::)) ->    ($#m1_hidden :::"set"::: )  , F3(  ($#m1_hidden :::"T-Sequence":::)) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set  "(" (Set F1 "("  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "B")) ")" ) ")" )))
 provided
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) ")" )) "iff" (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "L")) ")" )) & (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 F3 "(" (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "B")) ")" ) ")" ))  ")" )  ")" ))  ")" )))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) ")" )))
 proof 


end; 
theorem :: ORDINAL1:35 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "holds"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "B"))) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Var "B"))) "or" (Bool (Set (Var "B"))  ($#r2_xboole_0 :::"c<"::: )  (Set (Var "A")))  ")" )) ; 
 begin  definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"On"::: "X" ->    ($#m1_hidden :::"set"::: )   means :: ORDINAL1:def 9 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Ordinal":::))  ")" )  ")" )); func  :::"Lim"::: "X" ->    ($#m1_hidden :::"set"::: )   means :: ORDINAL1:def 10 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  "X") & (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )  ")" ))  ")" )  ")" )); end; 










:: deftheorem    defines :::"On"::: ORDINAL1:def 9 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Ordinal":::))  ")" )  ")" ))  ")" )); 
 
:: deftheorem    defines :::"Lim"::: ORDINAL1:def 10 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "b2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_ordinal1 :::"Lim"::: )  (Set (Var "X")))) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )  ")" ))  ")" )  ")" ))  ")" )); 
 
theorem :: ORDINAL1:36 (Bool  "for" (Set (Var "D")) "being"   ($#m1_hidden :::"Ordinal":::) (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "D"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )  ")" ))) ; 
 definitionfunc  :::"omega":::  ->    ($#m1_hidden :::"set"::: )   means :: ORDINAL1:def 11 (Bool  "("  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  it) & (Bool it "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) & (Bool it "is"   ($#v3_ordinal1 :::"ordinal"::: )  ) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool it  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" )  ")" ); end; 




:: deftheorem    defines :::"omega"::: ORDINAL1:def 11 :  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )) "iff" (Bool  "("  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "b1"))) & (Bool (Set (Var "b1")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) & (Bool (Set (Var "b1")) "is"   ($#v3_ordinal1 :::"ordinal"::: )  ) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Var "b1"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))  ")" )  ")" )  ")" )); 
 registration
cluster (Set   ($#k4_ordinal1 :::"omega"::: )  ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_ordinal1 :::"ordinal"::: )   ; 
end; definitionlet "A" be    ($#m1_hidden :::"set"::: )  ; attr "A" is  :::"natural":::  means :: ORDINAL1:def 12 (Bool "A"  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  )); end; 




:: deftheorem    defines :::"natural"::: ORDINAL1:def 12 :  (Bool  "for" (Set (Var "A")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v7_ordinal1 :::"natural"::: )  ) "iff" (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))  ")" )); 
 registration
cluster   ($#v7_ordinal1 :::"natural"::: )    for    ($#m1_hidden :::"number"::: )  ; 
end; definitionmode Nat is   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )  ; end; registration


  ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )  


(Bool  "ex" (Set (Var "b1")) "being"    ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "b2")) "being"   ($#v7_ordinal1 :::"natural"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "b2"))  ($#r2_hidden :::"in"::: )  (Set (Var "b1")))))
 
; 
end; registrationlet "A" be   ($#m1_hidden :::"Ordinal":::); 
cluster   ->   ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "A"; 
end; registration
cluster   ($#v7_ordinal1 :::"natural"::: )    ->   ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_hidden :::"number"::: )  ; 
end; scheme  :: ORDINAL1:sch 6 ALFA{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "d")))) & (Bool P1[(Set (Var "d")) "," (Set (Var "A"))]) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool P1[(Set (Var "d")) "," (Set (Var "B"))])) "holds"  (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))  ")" )  ")" ))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool P1[(Set (Var "d")) "," (Set (Var "A"))])))
 proof 


end; 
theorem :: ORDINAL1:37 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "X")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "X")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) ; 
 registration
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v7_ordinal1 :::"natural"::: )    for    ($#m1_hidden :::"number"::: )  ; 

cluster   ->   ($#v7_ordinal1 :::"natural"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k4_ordinal1 :::"omega"::: )  ); 
end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v7_ordinal1 :::"natural"::: )    for    ($#m1_hidden :::"number"::: )  ; 
end; registrationlet "a" be   ($#v7_ordinal1 :::"natural"::: )    ($#m1_hidden :::"Ordinal":::); 
cluster (Set   ($#k1_ordinal1 :::"succ"::: )  "a") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; registration
cluster   ($#v1_xboole_0 :::"empty"::: )    ->   ($#v6_ordinal1 :::"c=-linear"::: )    for    ($#m1_hidden :::"number"::: )  ; 
end; registrationlet "X" be   ($#v6_ordinal1 :::"c=-linear"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster   ->   ($#v6_ordinal1 :::"c=-linear"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  "X"); 
end;