:: ORDINAL4  semantic presentation begin  























registrationlet "L" be   ($#m1_hidden :::"Ordinal-Sequence":::); 
cluster (Set   ($#k1_ordinal2 :::"last"::: )  "L") ->   ($#v3_ordinal1 :::"ordinal"::: )   ; 
end; 
theorem :: ORDINAL4:1 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A"))))) "holds"  (Bool  "("  (Bool (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi")))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi"))) & (Bool (Set   ($#k8_ordinal2 :::"lim"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal2 :::"last"::: )  (Set (Var "fi"))))  ")" ))) ; 
 definitionlet "fi", "psi" be   ($#m1_hidden :::"T-Sequence":::); func "fi" :::"^"::: "psi" ->   ($#m1_hidden :::"T-Sequence":::) means :: ORDINAL4:def 1 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "fi" ")" )  ($#k10_ordinal2 :::"+^"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "psi" ")" ))) & (Bool  "("   "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "fi"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set "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   ($#k9_xtuple_0 :::"dom"::: )  "psi"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "fi" ")" )  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set "psi"  ($#k1_funct_1 :::"."::: )  (Set (Var "A"))))  ")" )  ")" ); end; 






:: deftheorem    defines :::"^"::: ORDINAL4:def 1 :  (Bool  "for" (Set (Var "fi")) "," (Set (Var "psi")) "," (Set (Var "b3")) "being"   ($#m1_hidden :::"T-Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "fi"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "psi")))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")) ")" )  ($#k10_ordinal2 :::"+^"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "psi")) ")" ))) & (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 "fi"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (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   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "psi"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")) ")" )  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "psi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A"))))  ")" )  ")" )  ")" )); 
 
theorem :: ORDINAL4:2 (Bool  "for" (Set (Var "fi")) "," (Set (Var "psi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "fi"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "psi")) ")" ))  ($#r1_tarski :::"c="::: )  (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "fi")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "psi")) ")" )))) ; 
 registrationlet "fi", "psi" be   ($#m1_hidden :::"Ordinal-Sequence":::); 
cluster (Set "fi"  ($#k1_ordinal4 :::"^"::: )  "psi") ->   ($#v1_ordinal2 :::"Ordinal-yielding"::: )   ; 
end; 
theorem :: ORDINAL4:3 (Bool  "for" (Set (Var "psi")) "," (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "psi")))) "holds"  (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Set (Var "fi"))  ($#k1_ordinal4 :::"^"::: )  (Set (Var "psi")))))) ; 
 
theorem :: ORDINAL4:4 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi")))) "holds"  (Bool (Set (Set (Var "B"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "A")))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Set (Var "B"))  ($#k1_ordinal3 :::"+^"::: )  (Set (Var "fi")))))) ; 
 
theorem :: ORDINAL4:5 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi")))) "holds"  (Bool (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "B")))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Set (Var "fi"))  ($#k4_ordinal3 :::"*^"::: )  (Set (Var "B")))))) ; 
 
theorem :: ORDINAL4:6 (Bool  "for" (Set (Var "fi")) "," (Set (Var "psi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "psi")))) & (Bool (Set (Var "B"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi"))) & (Bool (Set (Var "C"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "psi"))) & (Bool  "("  (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 "fi"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "psi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A"))))) "or" (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 "fi"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "psi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))))  ")" )) "holds"  (Bool (Set (Var "B"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "C"))))) ; 
 




theorem :: ORDINAL4:7 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f1")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f2")))) & (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "f1"))) & (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "f2"))) & (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 "fi"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))) & (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A"))))  ")" )  ")" )) "holds"  (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi")))))) ; 
 
theorem :: ORDINAL4:8 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi"))) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) & (Bool (Set (Var "fi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "fi")))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi"))) & (Bool (Set   ($#k8_ordinal2 :::"lim"::: )  (Set (Var "fi")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "fi"))))  ")" )) ; 
 
theorem :: ORDINAL4:9 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "fi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))))) ; 
 
theorem :: ORDINAL4:10 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "fi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))))) ; 
 
theorem :: ORDINAL4:11 (Bool  "for" (Set (Var "phi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "phi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  )) "holds"  (Bool (Set (Set (Var "phi"))  ($#k8_relat_1 :::"""::: )  (Set (Var "A"))) "is"   ($#m1_hidden :::"Ordinal":::)))) ; 
 
theorem :: ORDINAL4:12 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v2_ordinal2 :::"increasing"::: )  )) "holds"  (Bool (Set (Set (Var "f2"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f1"))) "is"   ($#m1_hidden :::"Ordinal-Sequence":::))) ; 
 
theorem :: ORDINAL4:13 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v2_ordinal2 :::"increasing"::: )  )) "holds"  (Bool  "ex" (Set (Var "phi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "st"  (Bool  "("  (Bool (Set (Var "phi"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f2")))) & (Bool (Set (Var "phi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  )  ")" ))) ; 
 
theorem :: ORDINAL4:14 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "f2"))) & (Bool (Set   ($#k3_ordinal2 :::"sup"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f1")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f2")))) & (Bool (Set (Var "fi"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f2"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f1"))))) "holds"  (Bool (Set (Var "A"))  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi")))))) ; 
 
theorem :: ORDINAL4:15 (Bool  "for" (Set (Var "phi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "phi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  )) "holds"  (Bool (Set (Set (Var "phi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "A"))) "is"   ($#v2_ordinal2 :::"increasing"::: )  ))) ; 
 
theorem :: ORDINAL4:16 (Bool  "for" (Set (Var "phi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "phi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "phi"))) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "phi"))) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) ; 
 
theorem :: ORDINAL4:17 (Bool  "for" (Set (Var "fi")) "," (Set (Var "psi")) "," (Set (Var "phi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set (Var "fi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set (Var "fi")) "is"   ($#v3_ordinal2 :::"continuous"::: )  ) & (Bool (Set (Var "psi")) "is"   ($#v3_ordinal2 :::"continuous"::: )  ) & (Bool (Set (Var "phi"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "psi"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "fi"))))) "holds"  (Bool (Set (Var "phi")) "is"   ($#v3_ordinal2 :::"continuous"::: )  )) ; 
 
theorem :: ORDINAL4:18 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (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 "fi"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "A"))))  ")" )) "holds"  (Bool (Set (Var "fi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ))) ; 
 
theorem :: ORDINAL4:19 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#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   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "C"))))  ")" )) "holds"  (Bool (Set (Var "fi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ))) ; 
 
theorem :: ORDINAL4:20 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ORDINAL4:21 (Bool  "for" (Set (Var "A")) "," (Set (Var "C")) "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"::: )  )) "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 "A"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "B")) ")" ))  ")" )) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")" )  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "fi"))))) ; 
 
theorem :: ORDINAL4:22 (Bool  "for" (Set (Var "C")) "," (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "C"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ORDINAL4:23 (Bool  "for" (Set (Var "C")) "," (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set  "("  ($#k1_ordinal1 :::"succ"::: )  (Set (Var "A")) ")" ) ")" ))) ; 
 
theorem :: ORDINAL4:24 (Bool  "for" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")" )  ($#r2_hidden :::"in"::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "B")) ")" ))) ; 
 
theorem :: ORDINAL4:25 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (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 "fi"))))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")" ))  ")" )) "holds"  (Bool (Set (Var "fi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ))) ; 
 
theorem :: ORDINAL4:26 (Bool  "for" (Set (Var "C")) "," (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "A")) "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 "A"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "fi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "B")) ")" ))  ")" )) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "fi")))))) ; 
 
theorem :: ORDINAL4:27 (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"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")" )  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "B")) ")" ))) ; 
 
theorem :: ORDINAL4:28 (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   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "A")) "," (Set (Var "C")) ")" )  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "B")) "," (Set (Var "C")) ")" ))) ; 
 
theorem :: ORDINAL4:29 (Bool  "for" (Set (Var "C")) "," (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")" ))) ; 
 
theorem :: ORDINAL4:30 (Bool  "for" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set  "(" (Set (Var "A"))  ($#k10_ordinal2 :::"+^"::: )  (Set (Var "B")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "B")) ")"  ")" )  ($#k11_ordinal2 :::"*^"::: )  (Set  "("  ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")"  ")" )))) ; 
 
theorem :: ORDINAL4:31 (Bool  "for" (Set (Var "C")) "," (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set  "("  ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")"  ")" ) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set  "(" (Set (Var "B"))  ($#k11_ordinal2 :::"*^"::: )  (Set (Var "A")) ")" ) ")" ))) ; 
 
theorem :: ORDINAL4:32 (Bool  "for" (Set (Var "C")) "," (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Num 1)  ($#r2_hidden :::"in"::: )  (Set (Var "C")))) "holds"  (Bool (Set (Var "A"))  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k12_ordinal2 :::"exp"::: )   "(" (Set (Var "C")) "," (Set (Var "A")) ")" ))) ; 
 scheme  :: ORDINAL4:sch 1 CriticalNumber{ F1(  ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_hidden :::"Ordinal":::) } : 
(Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st" (Bool (Set F1 "(" (Set (Var "A")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "A"))))
 provided
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set F1 "(" (Set (Var "A")) ")" )  ($#r2_hidden :::"in"::: )  (Set F1 "(" (Set (Var "B")) ")" )))
 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"::: )  )) "holds"  (Bool  "for" (Set (Var "phi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "phi")))  ($#r1_hidden :::"="::: )  (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "B"))  ($#r2_hidden :::"in"::: )  (Set (Var "A")))) "holds"  (Bool (Set (Set (Var "phi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "B")))  ($#r1_hidden :::"="::: )  (Set F1 "(" (Set (Var "B")) ")" ))  ")" )) "holds"  (Bool (Set F1 "(" (Set (Var "A")) ")" )  ($#r1_ordinal2 :::"is_limes_of"::: )  (Set (Var "phi")))))
 proof 


end; 


registrationlet "W" be   ($#m1_hidden :::"Universe":::); 
cluster   ($#v3_ordinal1 :::"ordinal"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "W"; 
end; definitionlet "W" be   ($#m1_hidden :::"Universe":::); mode Ordinal of "W" is   ($#v3_ordinal1 :::"ordinal"::: )     ($#m1_subset_1 :::"Element"::: )   "of" "W"; mode Ordinal-Sequence of "W" is   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k2_ordinal1 :::"On"::: )  "W" ")" ) "," (Set  "("  ($#k2_ordinal1 :::"On"::: )  "W" ")" ); end; registrationlet "W" be   ($#m1_hidden :::"Universe":::); 
cluster   ($#v1_ordinal1 :::"epsilon-transitive"::: )     ($#v2_ordinal1 :::"epsilon-connected"::: )     ($#v3_ordinal1 :::"ordinal"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" "W"; 
end; registrationlet "W" be   ($#m1_hidden :::"Universe":::); 
cluster (Set   ($#k2_ordinal1 :::"On"::: )  "W") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; registrationlet "W" be   ($#m1_hidden :::"Universe":::); 
cluster   ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set   ($#k2_ordinal1 :::"On"::: )  "W") "," (Set   ($#k2_ordinal1 :::"On"::: )  "W"))  ->   ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_ordinal2 :::"Ordinal-yielding"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k2_ordinal1 :::"On"::: )  "W" ")" ) "," (Set  "("  ($#k2_ordinal1 :::"On"::: )  "W" ")" ) ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 






scheme  :: ORDINAL4:sch 2 UOSLambda{ F1() ->   ($#m1_hidden :::"Universe":::), F2(   ($#m1_hidden :::"set"::: )  ) ->   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ) } : 
(Bool  "ex" (Set (Var "phi")) "being"   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set (Var "phi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "a")) ")" ))))
 proof 


end; definitionlet "W" be   ($#m1_hidden :::"Universe":::); func  :::"0-element_of"::: "W" ->   ($#m1_subset_1 :::"Ordinal":::) "of" "W" equals :: ORDINAL4:def 2 (Set   ($#k1_xboole_0 :::"{}"::: )  ); func  :::"1-element_of"::: "W" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Ordinal":::) "of" "W" equals :: ORDINAL4:def 3 (Num 1); let "phi" be   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Const "W")); let "A1" be   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Const "W")); :: original: :::"."::: redefine func "phi" :::"."::: "A1" ->   ($#m1_subset_1 :::"Ordinal":::) "of" "W"; end; 










:: deftheorem    defines :::"0-element_of"::: ORDINAL4:def 2 :  (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set   ($#k2_ordinal4 :::"0-element_of"::: )  (Set (Var "W")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))); 
 
:: deftheorem    defines :::"1-element_of"::: ORDINAL4:def 3 :  (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set   ($#k3_ordinal4 :::"1-element_of"::: )  (Set (Var "W")))  ($#r1_hidden :::"="::: )  (Num 1))); 
 definitionlet "W" be   ($#m1_hidden :::"Universe":::); let "p2", "p1" be   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Const "W")); :: original: :::"*"::: redefine func "p1" :::"*"::: "p2" ->   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" "W"; end; 
theorem :: ORDINAL4:33 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::) "holds"   (Bool  "("  (Bool (Set   ($#k2_ordinal4 :::"0-element_of"::: )  (Set (Var "W")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set   ($#k3_ordinal4 :::"1-element_of"::: )  (Set (Var "W")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )) ; 
 definitionlet "W" be   ($#m1_hidden :::"Universe":::); let "A1" be   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Const "W")); :: original: :::"succ"::: redefine func  :::"succ"::: "A1" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Ordinal":::) "of" "W"; let "B1" be   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Const "W")); :: original: :::"+^"::: redefine func "A1" :::"+^"::: "B1" ->   ($#m1_subset_1 :::"Ordinal":::) "of" "W"; end; definitionlet "W" be   ($#m1_hidden :::"Universe":::); let "A1", "B1" be   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Const "W")); :: original: :::"*^"::: redefine func "A1" :::"*^"::: "B1" ->   ($#m1_subset_1 :::"Ordinal":::) "of" "W"; end; 
theorem :: ORDINAL4:34 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "A1")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))  (Bool  "for" (Set (Var "phi")) "being"   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W")) "holds"  (Bool (Set (Var "A1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "phi"))))))) ; 
 
theorem :: ORDINAL4:35 (Bool  "for" (Set (Var "fi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "fi")))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "fi")))  ($#r1_tarski :::"c="::: )  (Set (Var "W")))) "holds"  (Bool (Set   ($#k4_ordinal2 :::"sup"::: )  (Set (Var "fi")))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))))) ; 
 



theorem :: ORDINAL4:36 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "phi")) "being"   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "phi")) "is"   ($#v2_ordinal2 :::"increasing"::: )  ) & (Bool (Set (Var "phi")) "is"   ($#v3_ordinal2 :::"continuous"::: )  ) & (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool  "ex" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "phi")))) & (Bool (Set (Set (Var "phi"))  ($#k1_funct_1 :::"."::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "A")))  ")" )))) ; 
 begin  




theorem :: ORDINAL4:37 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set (Var "C")))) "holds"  (Bool (Set (Var "A"))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set (Var "C")))) ; 
 
theorem :: ORDINAL4:38 (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"Ordinal":::)  "st" (Bool (Bool (Set (Var "A"))  ($#r2_ordinal2 :::"is_cofinal_with"::: )  (Set (Var "B")))) "holds"  (Bool  "("  (Bool (Set (Var "A")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) "iff" (Bool (Set (Var "B")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )  ")" )) ; 
 registrationlet "D" be   ($#m1_hidden :::"Ordinal":::); let "f", "g" be   ($#m1_hidden :::"T-Sequence":::) "of" (Set (Const "D")); 
cluster (Set "f"  ($#k1_ordinal4 :::"^"::: )  "g") -> "D"  ($#v5_relat_1 :::"-valued"::: )   ; 
end;