theorem Th5: :: ZFREFLE1:5

for M being non empty set st M |= ZF-axioms & M is epsilon-transitive holds
M is being_a_model_of_ZF