for M1, M2 being non empty set st M1 is being_a_model_of_ZF & M1 <==> M2 & M2 is epsilon-transitive holds
M2 is being_a_model_of_ZF