let M be non empty set ; :: thesis: ( M is being_a_model_of_ZF implies M |= ZF-axioms )
assume A1: ( M is epsilon-transitive & M |= the_axiom_of_pairs & M |= the_axiom_of_unions & M |= the_axiom_of_infinity & M |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
M |= the_axiom_of_substitution_for H ) ) ; :: according to ZF_MODEL:def 12 :: thesis: M |= ZF-axioms
let H be ZF-formula; :: according to ZFREFLE1:def 1 :: thesis: ( H in ZF-axioms implies M |= H )
assume H in ZF-axioms ; :: thesis: M |= H
then ( H = the_axiom_of_extensionality or H = the_axiom_of_pairs or H = the_axiom_of_unions or H = the_axiom_of_infinity or H = the_axiom_of_power_sets or ex H1 being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H1 & H = the_axiom_of_substitution_for H1 ) ) by Def4;
hence M |= H by A1, ZFMODEL1:1; :: thesis: verum