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