:: ORDINAL2  semantic presentation begin  



























scheme  :: ORDINAL2:sch 1 OrdinalInd{ P1[  ($#m1_hidden :::"Ordinal":::)] } : 
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool P1[(Set (Var "A"))]))
 provided
(Bool P1[(Set   ($#k1_xboole_0 :::"{}"::: )  )])
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))]))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool P1[(Set (Var "B"))])  ")" )) "holds"  (Bool P1[(Set (Var "A"))]))
 proof 


end; 
theorem :: ORDINAL2:1 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B"))) "iff" (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B"))))  ")" )) ; 
 
theorem :: ORDINAL2:2 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) ; 
 
theorem :: ORDINAL2:3 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_setfam_1 :::"bool"::: )  (Set (Var "A"))))) ; 
 
theorem :: ORDINAL2:4 (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) ; 
 
theorem :: ORDINAL2:5 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "A")))) ; 
 definitionlet "L" be   ($#m1_hidden :::"T-Sequence":::); func  :::"last"::: "L" ->    ($#m1_hidden :::"set"::: )   equals :: ORDINAL2:def 1 (Set "L"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "L" ")" ) ")" )); end; 





:: deftheorem    defines :::"last"::: ORDINAL2:def 1 :  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "holds"  (Bool (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")) ")" ) ")" )))); 
 
theorem :: ORDINAL2:6 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))))) ; 
 
theorem :: ORDINAL2:7 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) ; 
 
theorem :: ORDINAL2:8 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) ; 
 
theorem :: ORDINAL2:9 (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 (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "Y"))))) ; 
 
theorem :: ORDINAL2:10 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_ordinal1 :::"Lim"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) ; 
 
theorem :: ORDINAL2:11 (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 (Set   ($#k3_ordinal1 :::"Lim"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_ordinal1 :::"Lim"::: )  (Set (Var "Y"))))) ; 
 
theorem :: ORDINAL2:12 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_ordinal1 :::"Lim"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "X"))))) ; 
 
theorem :: ORDINAL2:13 (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 (Set (Var "x")) "is"   ($#m1_hidden :::"Ordinal":::))  ")" )) "holds"  (Bool (Set   ($#k1_setfam_1 :::"meet"::: )  (Set (Var "X"))) "is"   ($#m1_hidden :::"Ordinal":::))) ; 
 registration
cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )     ($#v4_ordinal1 :::"limit_ordinal"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"inf"::: "X" ->   ($#m1_hidden :::"Ordinal":::) equals :: ORDINAL2:def 2 (Set   ($#k1_setfam_1 :::"meet"::: )  (Set  "("  ($#k2_ordinal1 :::"On"::: )  "X" ")" )); func  :::"sup"::: "X" ->   ($#m1_hidden :::"Ordinal":::) means :: ORDINAL2:def 3 (Bool  "("  (Bool (Set   ($#k2_ordinal1 :::"On"::: )  "X")  ($#r1_tarski :::"c="::: )  it) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k2_ordinal1 :::"On"::: )  "X")  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool it  ($#r1_ordinal1 :::"c="::: )  (Set (Var "A")))  ")" )  ")" ); end; 










:: deftheorem    defines :::"inf"::: ORDINAL2:def 2 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_ordinal2 :::"inf"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_setfam_1 :::"meet"::: )  (Set  "("  ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")) ")" )))); 
 
:: deftheorem    defines :::"sup"::: ORDINAL2:def 3 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X")))) "iff" (Bool  "("  (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set (Var "b2"))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "b2"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "A")))  ")" )  ")" )  ")" ))); 
 
theorem :: ORDINAL2:14 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k2_ordinal2 :::"inf"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "A"))))) ; 
 
theorem :: ORDINAL2:15 (Bool  "for" (Set (Var "D")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "D"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "A")))  ")" )) "holds"  (Bool (Set (Var "D"))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k2_ordinal2 :::"inf"::: )  (Set (Var "X")))))) ; 
 
theorem :: ORDINAL2:16 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k2_ordinal2 :::"inf"::: )  (Set (Var "Y")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k2_ordinal2 :::"inf"::: )  (Set (Var "X")))))) ; 
 
theorem :: ORDINAL2:17 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set   ($#k2_ordinal2 :::"inf"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) ; 
 
theorem :: ORDINAL2:18 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) ; 
 
theorem :: ORDINAL2:19 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X")))))) ; 
 
theorem :: ORDINAL2:20 (Bool  "for" (Set (Var "D")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))  ")" )) "holds"  (Bool (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "D"))))) ; 
 
theorem :: ORDINAL2:21 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X"))))) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))  ")" )))) ; 
 
theorem :: ORDINAL2:22 (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 (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "Y"))))) ; 
 
theorem :: ORDINAL2:23 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k3_ordinal2 :::"sup"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "A")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) ; 
 
theorem :: ORDINAL2:24 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k2_ordinal2 :::"inf"::: )  (Set (Var "X")))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X"))))) ; 
 scheme  :: ORDINAL2:sch 2 TSLambda{ F1() ->   ($#m1_hidden :::"Ordinal":::), F2(  ($#m1_hidden :::"Ordinal":::)) ->    ($#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 "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) ")" ))  ")" )  ")" ))
 proof 


end; definitionlet "f" be   ($#m1_hidden :::"Function":::); attr "f" is  :::"Ordinal-yielding":::  means :: ORDINAL2:def 4 (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  "f")  ($#r1_tarski :::"c="::: )  (Set (Var "A")))); end; 




:: deftheorem    defines :::"Ordinal-yielding"::: ORDINAL2:def 4 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_ordinal2 :::"Ordinal-yielding"::: )  ) "iff" (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))))  ")" )); 
 registration
cluster   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_ordinal2 :::"Ordinal-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionmode Ordinal-Sequence is   ($#v1_ordinal2 :::"Ordinal-yielding"::: )    ($#m1_hidden :::"T-Sequence":::); end; registrationlet "A" be   ($#m1_hidden :::"Ordinal":::); 
cluster   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_relat_1 :::"Relation-like"::: )   "A"  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )    ->   ($#v1_ordinal2 :::"Ordinal-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "L" be   ($#m1_hidden :::"Ordinal-Sequence":::); let "A" be   ($#m1_hidden :::"Ordinal":::); 
cluster (Set "L"  ($#k5_relat_1 :::"|"::: )  "A") ->   ($#v1_ordinal2 :::"Ordinal-yielding"::: )   ; 
end; 




theorem :: ORDINAL2:25 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A"))) "is"   ($#m1_hidden :::"Ordinal":::)))) ; 
 registrationlet "f" be   ($#m1_hidden :::"Ordinal-Sequence":::); let "a" be   ($#m1_hidden :::"Ordinal":::); 
cluster (Set "f"  ($#k1_funct_1 :::"."::: )  "a") ->   ($#v3_ordinal1 :::"ordinal"::: )   ; 
end; scheme  :: ORDINAL2:sch 3 OSLambda{ F1() ->   ($#m1_hidden :::"Ordinal":::), F2(  ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::) } : 
(Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) ")" ))  ")" )  ")" ))
 proof 


end; scheme  :: ORDINAL2:sch 4 TSUniq1{ F1() ->   ($#m1_hidden :::"Ordinal":::), F2() ->    ($#m1_hidden :::"set"::: )  , F3(  ($#m1_hidden :::"Ordinal":::) ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->    ($#m1_hidden :::"set"::: )  , F5() ->   ($#m1_hidden :::"T-Sequence":::), F6() ->   ($#m1_hidden :::"T-Sequence":::) } : 
(Bool (Set F5 "("  ")" )  ($#r1_hidden :::"="::: )  (Set F6 "("  ")" ))
 provided
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F5 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))
 and  
 "("  (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "implies" (Bool (Set (Set F5 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))  ")" 
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool (Set (Set F5 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "A")) "," (Set  "(" (Set F5 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")) ")" ) ")" )))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set F5 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "A")) "," (Set  "(" (Set F5 "("  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "A")) ")" ) ")" )))
 and  
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F6 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))
 and  
 "("  (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "implies" (Bool (Set (Set F6 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))  ")" 
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool (Set (Set F6 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "A")) "," (Set  "(" (Set F6 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")) ")" ) ")" )))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set F6 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "A")) "," (Set  "(" (Set F6 "("  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "A")) ")" ) ")" )))
 proof 


end; scheme  :: ORDINAL2:sch 5 TSExist1{ F1() ->   ($#m1_hidden :::"Ordinal":::), F2() ->    ($#m1_hidden :::"set"::: )  , F3(  ($#m1_hidden :::"Ordinal":::) ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(  ($#m1_hidden :::"Ordinal":::) ","   ($#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 (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "implies" (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))  ")"  & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "A")) "," (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "A")) "," (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "A")) ")" ) ")" ))  ")" )  ")" ))
 proof 


end; scheme  :: ORDINAL2:sch 6 TSResult{ F1() ->   ($#m1_hidden :::"T-Sequence":::), F2(  ($#m1_hidden :::"Ordinal":::)) ->    ($#m1_hidden :::"set"::: )  , F3() ->   ($#m1_hidden :::"Ordinal":::), F4() ->    ($#m1_hidden :::"set"::: )  , F5(  ($#m1_hidden :::"Ordinal":::) ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F6(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->    ($#m1_hidden :::"set"::: )   } : 
(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")) ")" )))
 provided
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) ")" )) "iff" (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "L")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F4 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F6 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))  ")" )))
 and  
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F1 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "("  ")" ))
 and  
 "("  (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set F3 "("  ")" ))) "implies" (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F4 "("  ")" ))  ")" 
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set F3 "("  ")" ))) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "A")) "," (Set  "(" (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")) ")" ) ")" )))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set F3 "("  ")" )) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F6 "(" (Set (Var "A")) "," (Set  "(" (Set F1 "("  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "A")) ")" ) ")" )))
 proof 


end; scheme  :: ORDINAL2:sch 7 TSDef{ F1() ->   ($#m1_hidden :::"Ordinal":::), F2() ->    ($#m1_hidden :::"set"::: )  , F3(  ($#m1_hidden :::"Ordinal":::) ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "("  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )  (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "L")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))) & (Bool  "("   "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "L")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" )) & (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "x2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "L")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))) "holds"  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "x2")))  ")" )  ")" )
 proof 


end; scheme  :: ORDINAL2:sch 8 TSResult0{ F1(  ($#m1_hidden :::"Ordinal":::)) ->    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_hidden :::"set"::: )  , F3(  ($#m1_hidden :::"Ordinal":::) ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool (Set F1 "(" (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))
 provided
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set F1 "(" (Set (Var "A")) ")" )) "iff" (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "L")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))  ")" )))
 proof 


end; scheme  :: ORDINAL2:sch 9 TSResultS{ F1() ->    ($#m1_hidden :::"set"::: )  , F2(  ($#m1_hidden :::"Ordinal":::) ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F3(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->    ($#m1_hidden :::"set"::: )  , F4(  ($#m1_hidden :::"Ordinal":::)) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set F4 "(" (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) "," (Set F4 "(" (Set (Var "A")) ")" ) ")" )))
 provided
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "A")) ")" )) "iff" (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "L")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))  ")" )))
 proof 


end; scheme  :: ORDINAL2:sch 10 TSResultL{ F1() ->   ($#m1_hidden :::"T-Sequence":::), F2() ->   ($#m1_hidden :::"Ordinal":::), F3(  ($#m1_hidden :::"Ordinal":::)) ->    ($#m1_hidden :::"set"::: )  , F4() ->    ($#m1_hidden :::"set"::: )  , F5(  ($#m1_hidden :::"Ordinal":::) ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F6(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool (Set F3 "(" (Set F2 "("  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set F6 "(" (Set F2 "("  ")" ) "," (Set F1 "("  ")" ) ")" ))
 provided
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "A")) ")" )) "iff" (Bool  "ex" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "L")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F4 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F6 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))  ")" )))
 and  
(Bool  "("  (Bool (Set F2 "("  ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set F2 "("  ")" ) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )  ")" )
 and  
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F1 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" ))) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "A")) ")" )))
 proof 


end; scheme  :: ORDINAL2:sch 11 OSExist{ F1() ->   ($#m1_hidden :::"Ordinal":::), F2() ->   ($#m1_hidden :::"Ordinal":::), F3(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::), F4(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->   ($#m1_hidden :::"Ordinal":::) } : 
(Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) &  "("  (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "implies" (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))  ")"  & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "A")) "," (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "A")) "," (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "A")) ")" ) ")" ))  ")" )  ")" ))
 proof 


end; scheme  :: ORDINAL2:sch 12 OSResult{ F1() ->   ($#m1_hidden :::"Ordinal-Sequence":::), F2(  ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::), F3() ->   ($#m1_hidden :::"Ordinal":::), F4() ->   ($#m1_hidden :::"Ordinal":::), F5(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::), F6(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->   ($#m1_hidden :::"Ordinal":::) } : 
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) ")" )))
 provided
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) ")" )) "iff" (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F4 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F6 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))  ")" ))
 and  
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F1 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "("  ")" ))
 and  
 "("  (Bool (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set F3 "("  ")" ))) "implies" (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F4 "("  ")" ))  ")" 
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set F3 "("  ")" ))) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "A")) "," (Set  "(" (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")) ")" ) ")" )))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set F3 "("  ")" )) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F6 "(" (Set (Var "A")) "," (Set  "(" (Set F1 "("  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "A")) ")" ) ")" )))
 proof 


end; scheme  :: ORDINAL2:sch 13 OSDef{ F1() ->   ($#m1_hidden :::"Ordinal":::), F2() ->   ($#m1_hidden :::"Ordinal":::), F3(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::), F4(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->   ($#m1_hidden :::"Ordinal":::) } : 
(Bool  "("  (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)(Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))) & (Bool  "("   "for" (Set (Var "A1")) "," (Set (Var "A2")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "A1"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" )) & (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "A2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" )))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))) "holds"  (Bool (Set (Var "A1"))  ($#r1_hidden :::"="::: )  (Set (Var "A2")))  ")" )  ")" )
 proof 


end; scheme  :: ORDINAL2:sch 14 OSResult0{ F1(  ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::), F2() ->   ($#m1_hidden :::"Ordinal":::), F3(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::), F4(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->   ($#m1_hidden :::"Ordinal":::) } : 
(Bool (Set F1 "(" (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))
 provided
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set F1 "(" (Set (Var "A")) ")" )) "iff" (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))  ")" ))
 proof 


end; scheme  :: ORDINAL2:sch 15 OSResultS{ F1() ->   ($#m1_hidden :::"Ordinal":::), F2(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::), F3(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->   ($#m1_hidden :::"Ordinal":::), F4(  ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::) } : 
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set F4 "(" (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "A")) "," (Set F4 "(" (Set (Var "A")) ")" ) ")" )))
 provided
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "A")) ")" )) "iff" (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))  ")" ))
 proof 


end; scheme  :: ORDINAL2:sch 16 OSResultL{ F1() ->   ($#m1_hidden :::"Ordinal-Sequence":::), F2() ->   ($#m1_hidden :::"Ordinal":::), F3(  ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::), F4() ->   ($#m1_hidden :::"Ordinal":::), F5(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::), F6(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->   ($#m1_hidden :::"Ordinal":::) } : 
(Bool (Set F3 "(" (Set F2 "("  ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set F6 "(" (Set F2 "("  ")" ) "," (Set F1 "("  ")" ) ")" ))
 provided
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "A")) ")" )) "iff" (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F4 "("  ")" )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set F5 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set F6 "(" (Set (Var "C")) "," (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" ))  ")" )  ")" ))  ")" ))
 and  
(Bool  "("  (Bool (Set F2 "("  ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set F2 "("  ")" ) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )  ")" )
 and  
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F1 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" ))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" ))) "holds"  (Bool (Set (Set F1 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "A")) ")" )))
 proof 


end; definitionlet "L" be   ($#m1_hidden :::"T-Sequence":::); func  :::"sup"::: "L" ->   ($#m1_hidden :::"Ordinal":::) equals :: ORDINAL2:def 5 (Set   ($#k3_ordinal2 :::"sup"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  "L" ")" )); func  :::"inf"::: "L" ->   ($#m1_hidden :::"Ordinal":::) equals :: ORDINAL2:def 6 (Set   ($#k2_ordinal2 :::"inf"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  "L" ")" )); end; 










:: deftheorem    defines :::"sup"::: ORDINAL2:def 5 :  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "holds"  (Bool (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_ordinal2 :::"sup"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "L")) ")" )))); 
 
:: deftheorem    defines :::"inf"::: ORDINAL2:def 6 :  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "holds"  (Bool (Set   ($#k5_ordinal2 :::"inf"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal2 :::"inf"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "L")) ")" )))); 
 
theorem :: ORDINAL2:26 (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::) "holds"   (Bool  "("  (Bool (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_ordinal2 :::"sup"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "L")) ")" ))) & (Bool (Set   ($#k5_ordinal2 :::"inf"::: )  (Set (Var "L")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal2 :::"inf"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "L")) ")" )))  ")" )) ; 
 definitionlet "L" be   ($#m1_hidden :::"T-Sequence":::); func  :::"lim_sup"::: "L" ->   ($#m1_hidden :::"Ordinal":::) means :: ORDINAL2:def 7 (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k5_ordinal2 :::"inf"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "L")) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "L"))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_ordinal2 :::"sup"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" "L"  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "L" ")" )  ($#k6_subset_1 :::"\"::: )  (Set (Var "A")) ")" ) ")" ) ")" )))  ")" )  ")" )); func  :::"lim_inf"::: "L" ->   ($#m1_hidden :::"Ordinal":::) means :: ORDINAL2:def 8 (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "L")) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "L"))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal2 :::"inf"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" "L"  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "L" ")" )  ($#k6_subset_1 :::"\"::: )  (Set (Var "A")) ")" ) ")" ) ")" )))  ")" )  ")" )); end; 










:: deftheorem    defines :::"lim_sup"::: ORDINAL2:def 7 :  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_ordinal2 :::"lim_sup"::: )  (Set (Var "L")))) "iff" (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_ordinal2 :::"inf"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_ordinal2 :::"sup"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set (Var "A")) ")" ) ")" ) ")" )))  ")" )  ")" ))  ")" ))); 
 
:: deftheorem    defines :::"lim_inf"::: ORDINAL2:def 8 :  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_ordinal2 :::"lim_inf"::: )  (Set (Var "L")))) "iff" (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal2 :::"inf"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set (Var "A")) ")" ) ")" ) ")" )))  ")" )  ")" ))  ")" ))); 
 definitionlet "A" be   ($#m1_hidden :::"Ordinal":::); let "fi" be   ($#m1_hidden :::"Ordinal-Sequence":::); pred "A" :::"is_limes_of"::: "fi" means :: ORDINAL2:def 9 (Bool  "ex" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "fi")) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "C"))) & (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "fi"))) "holds"  (Bool (Set "fi"  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  ")" )) if (Bool "A"  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  otherwise (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  "A") & (Bool "A"  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool  "ex" (Set (Var "D")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "D"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "fi")) & (Bool  "("   "for" (Set (Var "E")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "D"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "E"))) & (Bool (Set (Var "E"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "fi"))) "holds"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set "fi"  ($#k1_funct_1 :::"."::: )  (Set (Var "E")))) & (Bool (Set "fi"  ($#k1_funct_1 :::"."::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))  ")" )  ")" )  ")" ))); end; 





:: deftheorem    defines :::"is_limes_of"::: ORDINAL2:def 9 :  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi"))) "iff" (Bool  "ex" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "C"))) & (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi"))) "iff" (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A"))) & (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool  "ex" (Set (Var "D")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "D"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))) & (Bool  "("   "for" (Set (Var "E")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "D"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "E"))) & (Bool (Set (Var "E"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi"))))) "holds"  (Bool  "("  (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "E")))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "E")))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))  ")" )  ")" )  ")" )))  ")" )  ")"   ")" ))); 
 definitionlet "fi" be   ($#m1_hidden :::"Ordinal-Sequence":::); given "A" being   ($#m1_hidden :::"Ordinal":::) such that 
(Bool (Set (Const "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Const "fi")))
 ; func  :::"lim"::: "fi" ->   ($#m1_hidden :::"Ordinal":::) means :: ORDINAL2:def 10 (Bool it  ($#r1_ordinal2 :::"is_limes_of"::: )  "fi"); end; 






:: deftheorem    defines :::"lim"::: ORDINAL2:def 10 :  (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi"))))) "holds"  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_ordinal2 :::"lim"::: )  (Set (Var "fi")))) "iff" (Bool (Set (Var "b2"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi")))  ")" ))); 
 definitionlet "A" be   ($#m1_hidden :::"Ordinal":::); let "fi" be   ($#m1_hidden :::"Ordinal-Sequence":::); func  :::"lim":::  "(" "A" "," "fi" ")"  ->   ($#m1_hidden :::"Ordinal":::) equals :: ORDINAL2:def 11 (Set   ($#k8_ordinal2 :::"lim"::: )  (Set  "(" "fi"  ($#k5_relat_1 :::"|"::: )  "A" ")" )); end; 






:: deftheorem    defines :::"lim"::: ORDINAL2:def 11 :  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"  (Bool (Set   ($#k9_ordinal2 :::"lim"::: )   "(" (Set (Var "A")) "," (Set (Var "fi")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_ordinal2 :::"lim"::: )  (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "A")) ")" ))))); 
 definitionlet "L" be   ($#m1_hidden :::"Ordinal-Sequence":::); attr "L" is  :::"increasing":::  means :: ORDINAL2:def 12 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "L"))) "holds"  (Bool (Set "L"  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set "L"  ($#k1_funct_1 :::"."::: )  (Set (Var "B"))))); attr "L" is  :::"continuous":::  means :: ORDINAL2:def 13 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "L")) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set "L"  ($#k1_funct_1 :::"."::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Var "B"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set "L"  ($#k5_relat_1 :::"|"::: )  (Set (Var "A"))))); end; 








:: deftheorem    defines :::"increasing"::: ORDINAL2:def 12 :  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L"))))) "holds"  (Bool (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))))  ")" )); 
 
:: deftheorem    defines :::"continuous"::: ORDINAL2:def 13 :  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "L")) "is"   ($#v3_ordinal2 :::"continuous"::: )  ) "iff" (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L")))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) & (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "L"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Var "B"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "A")))))  ")" )); 
 definitionlet "A", "B" be   ($#m1_hidden :::"Ordinal":::); func "A" :::"+^"::: "B" ->   ($#m1_hidden :::"Ordinal":::) means :: ORDINAL2:def 14 (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "B")) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  "A") & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "B"))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "B")) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" )))  ")" )  ")" )); end; 






:: deftheorem    defines :::"+^"::: ORDINAL2:def 14 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "b3")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "B")))) "iff" (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" )))  ")" )  ")" ))  ")" )); 
 definitionlet "A", "B" be   ($#m1_hidden :::"Ordinal":::); func "A" :::"*^"::: "B" ->   ($#m1_hidden :::"Ordinal":::) means :: ORDINAL2:def 15 (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "A")) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "A"))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" )  ($#k10_ordinal2 :::"+^"::: )  "B"))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "A")) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k4_ordinal2 :::"sup"::: )  (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" )))  ")" )  ")" )); end; 






:: deftheorem    defines :::"*^"::: ORDINAL2:def 15 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "b3")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "B")))) "iff" (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" )  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "B"))))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k4_ordinal2 :::"sup"::: )  (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" ) ")" )))  ")" )  ")" ))  ")" )); 
 registrationlet "O" be   ($#m1_hidden :::"Ordinal":::); 
cluster   ->   ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "O"; 
end; definitionlet "A", "B" be   ($#m1_hidden :::"Ordinal":::); func  :::"exp":::  "(" "A" "," "B" ")"  ->   ($#m1_hidden :::"Ordinal":::) means :: ORDINAL2:def 16 (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "B")) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "B"))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set "A"  ($#k11_ordinal2 :::"*^"::: )  (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "B")) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_ordinal2 :::"lim"::: )  (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" )))  ")" )  ")" )); end; 






:: deftheorem    defines :::"exp"::: ORDINAL2:def 16 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "b3")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )) "iff" (Bool  "ex" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Num 1)) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "C")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set  "(" (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")) ")" )))  ")" ) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")))) & (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "C")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k8_ordinal2 :::"lim"::: )  (Set  "(" (Set (Var "fi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" )))  ")" )  ")" ))  ")" )); 
 
theorem :: ORDINAL2:27 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) ; 
 
theorem :: ORDINAL2:28 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set  "(" (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "B")) ")" )))) ; 
 
theorem :: ORDINAL2:29 (Bool  "for" (Set (Var "B")) "," (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "B")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set (Var "B"))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "C"))))  ")" )) "holds"  (Bool (Set (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "fi")))))) ; 
 
theorem :: ORDINAL2:30 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set  ($#k1_xboole_0 :::"{}"::: ) )  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) ; 
 
theorem :: ORDINAL2:31 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) ; 
 
theorem :: ORDINAL2:32 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "C"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "B"))))) ; 
 
theorem :: ORDINAL2:33 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "C"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "C"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "B"))))) ; 
 
theorem :: ORDINAL2:34 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "C")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "B"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "C"))))) ; 
 
theorem :: ORDINAL2:35 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set  ($#k1_xboole_0 :::"{}"::: ) )  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ORDINAL2:36 (Bool  "for" (Set (Var "B")) "," (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")) ")" )  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "B"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "A")) ")" )  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "A"))))) ; 
 
theorem :: ORDINAL2:37 (Bool  "for" (Set (Var "B")) "," (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "B")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set (Var "B"))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "A"))))  ")" )) "holds"  (Bool (Set (Set (Var "B"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k4_ordinal2 :::"sup"::: )  (Set (Var "fi")) ")" ))))) ; 
 
theorem :: ORDINAL2:38 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ORDINAL2:39 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Num 1)  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "A")))  ")" )) ; 
 
theorem :: ORDINAL2:40 (Bool  "for" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "C")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "B"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "C"))))) ; 
 
theorem :: ORDINAL2:41 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "C")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "B"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "C"))))) ; 
 
theorem :: ORDINAL2:42 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "C"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "C"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "B"))))) ; 
 
theorem :: ORDINAL2:43 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "A")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" )  ($#r1_hidden :::"="::: )  (Num 1))) ; 
 
theorem :: ORDINAL2:44 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "A")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "B")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set  "("  ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" )))) ; 
 
theorem :: ORDINAL2:45 (Bool  "for" (Set (Var "B")) "," (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "B")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set (Var "B"))) & (Bool  "("   "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "A")) "," (Set (Var "C")) ")" ))  ")" )) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k8_ordinal2 :::"lim"::: )  (Set (Var "fi")))))) ; 
 
theorem :: ORDINAL2:46 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "A")) "," (Num 1) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Num 1) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 
theorem :: ORDINAL2:47 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) (Bool  "ex" (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "B")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) & (Bool (Set (Var "C")) "is"   ($#v7_ordinal1 :::"natural"::: )  ) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "B"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "C"))))  ")" ))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "o" be   ($#m1_hidden :::"Ordinal":::); 
cluster (Set "X"  ($#k2_funcop_1 :::"-->"::: )  "o") ->   ($#v1_ordinal2 :::"Ordinal-yielding"::: )   ; 
end; registrationlet "O" be   ($#m1_hidden :::"Ordinal":::); let "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "O"  ($#k2_funcop_1 :::"-->"::: )  "x") ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )   ; 
end; definitionlet "A", "B" be   ($#m1_hidden :::"Ordinal":::); pred "A" :::"is_cofinal_with"::: "B" means :: ORDINAL2:def 17 (Bool  "ex" (Set (Var "xi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "xi")))  ($#r1_hidden :::"="::: )  "B") & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "xi")))  ($#r1_tarski :::"c="::: )  "A") & (Bool (Set (Var "xi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool "A"  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "xi"))))  ")" )); reflexivity  
(Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) (Bool  "ex" (Set (Var "xi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "xi")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "xi")))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "xi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "xi"))))  ")" )))
 ; end; 





:: deftheorem    defines :::"is_cofinal_with"::: ORDINAL2:def 17 :  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"   (Bool  "("  (Bool (Set (Var "A"))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set (Var "B"))) "iff" (Bool  "ex" (Set (Var "xi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "xi")))  ($#r1_hidden :::"="::: )  (Set (Var "B"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "xi")))  ($#r1_tarski :::"c="::: )  (Set (Var "A"))) & (Bool (Set (Var "xi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "xi"))))  ")" ))  ")" )); 
 




theorem :: ORDINAL2:48 (Bool  "for" (Set (Var "psi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "psi"))))) "holds"  (Bool (Set (Var "e")) "is"   ($#m1_hidden :::"Ordinal":::)))) ; 
 
theorem :: ORDINAL2:49 (Bool  "for" (Set (Var "psi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "psi")))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "psi"))))) ; 
 
theorem :: ORDINAL2:50 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 scheme  :: ORDINAL2:sch 17 OmegaInd{ F1() ->   ($#m1_hidden :::"Nat":::), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool P1[(Set F1 "("  ")" )])
 provided
(Bool P1[(Set   ($#k1_xboole_0 :::"{}"::: )  )])
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool P1[(Set (Var "a"))])) "holds"  (Bool P1[(Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "a")))]))
 proof 


end; registrationlet "a", "b" be   ($#m1_hidden :::"Nat":::); 
cluster (Set "a"  ($#k10_ordinal2 :::"+^"::: )  "b") ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; registrationlet "x", "y" be    ($#m1_hidden :::"set"::: )  ; let "a", "b" be   ($#m1_hidden :::"Nat":::); 
cluster (Set   ($#k14_funcop_1 :::"IFEQ"::: )   "(" "x" "," "y" "," "a" "," "b" ")" ) ->   ($#v7_ordinal1 :::"natural"::: )   ; 
end; scheme  :: ORDINAL2:sch 18 LambdaRecEx{ F1() ->    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )   ","    ($#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   ($#k4_ordinal1 :::"omega"::: )  )) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "n")) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ")" ))  ")" )  ")" ))
 proof 


end; 


scheme  :: ORDINAL2:sch 19 RecUn{ F1() ->    ($#m1_hidden :::"set"::: )  , F2() ->   ($#m1_hidden :::"Function":::), F3() ->   ($#m1_hidden :::"Function":::), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set F2 "("  ")" )  ($#r1_hidden :::"="::: )  (Set F3 "("  ")" ))
 provided
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F2 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))
 and  
(Bool (Set (Set F2 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "n")) "," (Set (Set F2 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "," (Set (Set F2 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "n")) ")" ))]))
 and  
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F3 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))
 and  
(Bool (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool P1[(Set (Var "n")) "," (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))) "," (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "n")) ")" ))]))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool P1[(Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y1"))]) & (Bool P1[(Set (Var "n")) "," (Set (Var "x")) "," (Set (Var "y2"))])) "holds"  (Bool (Set (Var "y1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))))
 proof 


end; scheme  :: ORDINAL2:sch 20 LambdaRecUn{ F1() ->    ($#m1_hidden :::"set"::: )  , F2(   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F3() ->   ($#m1_hidden :::"Function":::), F4() ->   ($#m1_hidden :::"Function":::) } : 
(Bool (Set F3 "("  ")" )  ($#r1_hidden :::"="::: )  (Set F4 "("  ")" ))
 provided
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F3 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))
 and  
(Bool (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "n")) "," (Set  "(" (Set F3 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )))
 and  
(Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F4 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal1 :::"omega"::: )  ))
 and  
(Bool (Set (Set F4 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" ))
 and  
(Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set F4 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "n")) "," (Set  "(" (Set F4 "("  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "n")) ")" ) ")" )))
 proof 


end;