let W be Universe; :: thesis: ( omega in W implies W is being_a_model_of_ZF )
assume omega in W ; :: thesis: W is being_a_model_of_ZF
hence ( W is epsilon-transitive & W |= the_axiom_of_pairs & W |= the_axiom_of_unions & W |= the_axiom_of_infinity & W |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
W |= the_axiom_of_substitution_for H ) ) by Th1, Th2, Th3, Th4, Th5; :: according to ZF_MODEL:def 12 :: thesis: verum