:: ZF_REFLE  semantic presentation begin  






















theorem :: ZF_REFLE:1 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set (Var "W"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k7_zf_model :::"the_axiom_of_pairs"::: )  ))) ; 
 
theorem :: ZF_REFLE:2 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set (Var "W"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k8_zf_model :::"the_axiom_of_unions"::: )  ))) ; 
 
theorem :: ZF_REFLE:3 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set (Var "W"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k9_zf_model :::"the_axiom_of_infinity"::: )  ))) ; 
 
theorem :: ZF_REFLE:4 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::) "holds"  (Bool (Set (Var "W"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k10_zf_model :::"the_axiom_of_power_sets"::: )  ))) ; 
 
theorem :: ZF_REFLE:5 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::)  "st" (Bool (Bool (Set  ($#k1_enumset1 :::"{"::: ) (Set  "("  ($#k2_zf_lang :::"x."::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set  "("  ($#k2_zf_lang :::"x."::: )  (Num 1) ")" ) "," (Set  "("  ($#k2_zf_lang :::"x."::: )  (Num 2) ")" ) ($#k1_enumset1 :::"}"::: ) )  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k2_zf_model :::"Free"::: )  (Set (Var "H"))))) "holds"  (Bool (Set (Var "W"))  ($#r2_zf_model :::"|="::: )  (Set   ($#k11_zf_model :::"the_axiom_of_substitution_for"::: )  (Set (Var "H")))))) ; 
 
theorem :: ZF_REFLE:6 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set (Var "W")) "is"   ($#v1_zf_model :::"being_a_model_of_ZF"::: )  )) ; 
 























scheme  :: ZF_REFLE:sch 1 ALFA9Universe{ F1() ->   ($#m1_hidden :::"Universe":::), F2() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "d")))) & (Bool P1[(Set (Var "d")) "," (Set (Var "a"))]) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "d")) "," (Set (Var "b"))])) "holds"  (Bool (Set (Var "a"))  ($#r1_ordinal1 :::"c="::: )  (Set (Var "b")))  ")" )  ")" ))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F2 "("  ")" ) (Bool  "ex" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ) "st" (Bool P1[(Set (Var "d")) "," (Set (Var "a"))])))
 proof 


end; 
theorem :: ZF_REFLE:7 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x")) "is"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))) "iff" (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "W"))))  ")" ))) ; 
 


scheme  :: ZF_REFLE:sch 2 OrdSeqOfUnivEx{ F1() ->   ($#m1_hidden :::"Universe":::), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(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 P1[(Set (Var "a")) "," (Set (Set (Var "phi"))  ($#k4_ordinal4 :::"."::: )  (Set (Var "a")))])))
 provided
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ) (Bool  "ex" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ) "st" (Bool P1[(Set (Var "a")) "," (Set (Var "b"))])))
 proof 


end; scheme  :: ZF_REFLE:sch 3 UOSExist{ F1() ->   ($#m1_hidden :::"Universe":::), F2() ->   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ), F3(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"Ordinal":::)) ->   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ), F4(  ($#m1_hidden :::"Ordinal":::) ","   ($#m1_hidden :::"T-Sequence":::)) ->   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ) } : 
(Bool  "ex" (Set (Var "phi")) "being"   ($#m1_subset_1 :::"Ordinal-Sequence":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "phi"))  ($#k4_ordinal4 :::"."::: )  (Set  "("  ($#k2_ordinal4 :::"0-element_of"::: )  (Set F1 "("  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ) "holds"  (Bool (Set (Set (Var "phi"))  ($#k4_ordinal4 :::"."::: )  (Set  "("  ($#k6_ordinal4 :::"succ"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "a")) "," (Set  "(" (Set (Var "phi"))  ($#k4_ordinal4 :::"."::: )  (Set (Var "a")) ")" ) ")" ))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_ordinal4 :::"0-element_of"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Var "a")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  )) "holds"  (Bool (Set (Set (Var "phi"))  ($#k4_ordinal4 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set F4 "(" (Set (Var "a")) "," (Set  "(" (Set (Var "phi"))  ($#k5_relset_1 :::"|"::: )  (Set (Var "a")) ")" ) ")" ))  ")" )  ")" ))
 proof 


end; scheme  :: ZF_REFLE:sch 4 UniverseInd{ F1() ->   ($#m1_hidden :::"Universe":::), P1[  ($#m1_hidden :::"Ordinal":::)] } : 
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set (Var "a"))]))
 provided
(Bool P1[(Set   ($#k2_ordinal4 :::"0-element_of"::: )  (Set F1 "("  ")" ))])
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "a"))])) "holds"  (Bool P1[(Set   ($#k6_ordinal4 :::"succ"::: )  (Set (Var "a")))]))
 and  
(Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k2_ordinal4 :::"0-element_of"::: )  (Set F1 "("  ")" ))) & (Bool (Set (Var "a")) "is"   ($#v4_ordinal1 :::"limit_ordinal"::: )  ) & (Bool  "("   "for" (Set (Var "b")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set F1 "("  ")" )  "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; definitionlet "f" be   ($#m1_hidden :::"Function":::); let "W" be   ($#m1_hidden :::"Universe":::); let "a" be   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Const "W")); func  :::"union":::  "(" "f" "," "a" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: ZF_REFLE:def 1 (Set   ($#k3_card_3 :::"Union"::: )  (Set  "(" "W"  ($#k6_relat_1 :::"|`"::: )  (Set  "(" "f"  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  "a" ")" ) ")" ) ")" )); end; 







:: deftheorem    defines :::"union"::: ZF_REFLE:def 1 :  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W")) "holds"  (Bool (Set   ($#k1_zf_refle :::"union"::: )   "(" (Set (Var "f")) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set (Var "W"))  ($#k6_relat_1 :::"|`"::: )  (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set (Var "a")) ")" ) ")" ) ")" )))))); 
 
theorem :: ZF_REFLE:8 (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"T-Sequence":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set (Var "A")) ")" )) "is"   ($#m1_hidden :::"T-Sequence":::)))) ; 
 
theorem :: ZF_REFLE:9 (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set (Var "A")) ")" )) "is"   ($#m1_hidden :::"Ordinal-Sequence":::)))) ; 
 
theorem :: ZF_REFLE:10 (Bool  "for" (Set (Var "psi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"  (Bool (Set   ($#k3_card_3 :::"Union"::: )  (Set (Var "psi"))) "is"   ($#m1_hidden :::"Ordinal":::))) ; 
 
theorem :: ZF_REFLE:11 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "psi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"  (Bool (Set   ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set (Var "X"))  ($#k6_relat_1 :::"|`"::: )  (Set (Var "psi")) ")" )) "is"   ($#m1_hidden :::"Ordinal":::)))) ; 
 
theorem :: ZF_REFLE:12 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::) "holds"  (Bool (Set   ($#k2_ordinal1 :::"On"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "A")))) ; 
 
theorem :: ZF_REFLE:13 (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"Ordinal":::)  (Bool  "for" (Set (Var "psi")) "being"   ($#m1_hidden :::"Ordinal-Sequence":::) "holds"  (Bool (Set (Set (Var "psi"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k4_classes1 :::"Rank"::: )  (Set (Var "A")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "psi"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "A")))))) ; 
 definitionlet "phi" be   ($#m1_hidden :::"Ordinal-Sequence":::); let "W" be   ($#m1_hidden :::"Universe":::); let "a" be   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Const "W")); :: original: :::"union"::: redefine func  :::"union":::  "(" "phi" "," "a" ")"  ->   ($#m1_subset_1 :::"Ordinal":::) "of" "W"; end; 
theorem :: ZF_REFLE:14 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "a")) "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  "("  (Bool (Set   ($#k2_zf_refle :::"union"::: )   "(" (Set (Var "phi")) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set (Var "phi"))  ($#k5_relset_1 :::"|"::: )  (Set (Var "a")) ")" ))) & (Bool (Set   ($#k2_zf_refle :::"union"::: )   "(" (Set  "(" (Set (Var "phi"))  ($#k5_relset_1 :::"|"::: )  (Set (Var "a")) ")" ) "," (Set (Var "a")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set (Var "phi"))  ($#k5_relset_1 :::"|"::: )  (Set (Var "a")) ")" )))  ")" )))) ; 
 definitionlet "W" be   ($#m1_hidden :::"Universe":::); let "a", "b" be   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Const "W")); :: original: :::"\/"::: redefine func "a" :::"\/"::: "b" ->   ($#m1_subset_1 :::"Ordinal":::) "of" "W"; end; registrationlet "W" be   ($#m1_hidden :::"Universe":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" "W"; 
end; definitionlet "W" be   ($#m1_hidden :::"Universe":::); mode Subclass of "W" is  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" "W"; end; definitionlet "W" be   ($#m1_hidden :::"Universe":::); let "IT" be   ($#m1_hidden :::"T-Sequence":::) "of" (Set (Const "W")); attr "IT" is  :::"DOMAIN-yielding":::  means :: ZF_REFLE:def 2 (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  "IT")  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal1 :::"On"::: )  "W")); end; 





:: deftheorem    defines :::"DOMAIN-yielding"::: ZF_REFLE:def 2 :  (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_hidden :::"T-Sequence":::) "of" (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_zf_refle :::"DOMAIN-yielding"::: )  ) "iff" (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "IT")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_ordinal1 :::"On"::: )  (Set (Var "W"))))  ")" ))); 
 registrationlet "W" be   ($#m1_hidden :::"Universe":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v2_relat_1 :::"non-empty"::: )   "W"  ($#v5_relat_1 :::"-valued"::: )     ($#v5_ordinal1 :::"T-Sequence-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_zf_refle :::"DOMAIN-yielding"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "W" be   ($#m1_hidden :::"Universe":::); mode DOMAIN-Sequence of "W" is   ($#v2_relat_1 :::"non-empty"::: )     ($#v1_zf_refle :::"DOMAIN-yielding"::: )    ($#m1_hidden :::"T-Sequence":::) "of" "W"; end; definitionlet "W" be   ($#m1_hidden :::"Universe":::); let "L" be   ($#m1_hidden :::"DOMAIN-Sequence":::) "of" (Set (Const "W")); :: original: :::"Union"::: redefine func  :::"Union"::: "L" ->   ($#m1_subset_1 :::"Subclass":::) "of" "W"; let "a" be   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Const "W")); :: original: :::"."::: redefine func "L" :::"."::: "a" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_subset_1 :::"Element"::: )   "of" "W"; end; 









theorem :: ZF_REFLE:15 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"DOMAIN-Sequence":::) "of" (Set (Var "W")) "holds"  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "L"))))))) ; 
 
theorem :: ZF_REFLE:16 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"DOMAIN-Sequence":::) "of" (Set (Var "W")) "holds"  (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_zf_refle :::"Union"::: )  (Set (Var "L"))))))) ; 
 
theorem :: ZF_REFLE:17 (Bool (Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set   ($#k1_zf_lang :::"VAR"::: )  )  ($#r2_tarski :::"are_equipotent"::: )  ) ; 
 
theorem :: ZF_REFLE:18 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set  "("  ($#k3_tarski :::"union"::: )  (Set  "("  ($#k2_ordinal1 :::"On"::: )  (Set (Var "X")) ")" ) ")" )))) ; 
 
theorem :: ZF_REFLE:19 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))) "holds"  (Bool (Set   ($#k3_ordinal2 :::"sup"::: )  (Set (Var "X")))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))))) ; 
 



theorem :: ZF_REFLE:20 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Universe":::)  (Bool  "for" (Set (Var "L")) "being"   ($#m1_hidden :::"DOMAIN-Sequence":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set   ($#k4_ordinal1 :::"omega"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool  "("   "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set (Var "b")))) "holds"  (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "b"))))  ")" ) & (Bool  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))  "st" (Bool (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"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_card_3 :::"Union"::: )  (Set  "(" (Set (Var "L"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "a")) ")" )))  ")" )) "holds"  (Bool  "for" (Set (Var "H")) "being"   ($#m2_finseq_1 :::"ZF-formula":::) (Bool  "ex" (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  "("   "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Ordinal":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Set (Var "phi"))  ($#k4_ordinal4 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r1_hidden :::"<>"::: )  (Set (Var "a")))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k1_zf_lang :::"VAR"::: ) ) "," (Set  "(" (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a")) ")" ) "holds"   (Bool  "("  (Bool (Set   ($#k4_zf_refle :::"Union"::: )  (Set (Var "L"))) "," (Set (Set  "("  ($#k4_zf_refle :::"Union"::: )  (Set (Var "L")) ")" )  ($#k1_zf_lang1 :::"!"::: )  (Set (Var "f")))  ($#r1_zf_model :::"|="::: )  (Set (Var "H"))) "iff" (Bool (Set (Set (Var "L"))  ($#k5_zf_refle :::"."::: )  (Set (Var "a"))) "," (Set (Var "f"))  ($#r1_zf_model :::"|="::: )  (Set (Var "H")))  ")" ))  ")" )  ")" ))))) ; 
 begin  



theorem :: ZF_REFLE:21 (Bool  "for" (Set (Var "M")) "being"  ($#~v4_card_3  "non"   ($#v4_card_3 :::"countable"::: )   )   ($#m1_hidden :::"Aleph":::)  "st" (Bool (Bool (Set (Var "M")) "is"   ($#v6_card_fil :::"strongly_inaccessible"::: )  )) "holds"  (Bool (Set   ($#k4_classes1 :::"Rank"::: )  (Set (Var "M"))) "is"   ($#v1_zf_model :::"being_a_model_of_ZF"::: )  )) ;