let E be non empty set ; :: thesis: ( E is epsilon-transitive & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ) implies E is being_a_model_of_ZF )
assume ( E is epsilon-transitive & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st
( u <> {} & ( for v being Element of E st v in u holds
ex w being Element of E st
( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E ) ) ; :: thesis: E is being_a_model_of_ZF
hence ( E is epsilon-transitive & E |= the_axiom_of_pairs & E |= the_axiom_of_unions & E |= the_axiom_of_infinity & E |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) ) by Th2, Th4, Th6, Th8, Th19; :: according to ZF_MODEL:def 12 :: thesis: verum