let M1, M2 be non empty set ; :: thesis: ( M1 is being_a_model_of_ZF & M1 <==> M2 & M2 is epsilon-transitive implies M2 is being_a_model_of_ZF )
assume that
A1: M1 is being_a_model_of_ZF and
A2: M1 <==> M2 ; :: thesis: ( not M2 is epsilon-transitive or M2 is being_a_model_of_ZF )
M1 |= ZF-axioms by A1, Th4;
then M2 |= ZF-axioms by A2, Th8;
hence ( not M2 is epsilon-transitive or M2 is being_a_model_of_ZF ) by Th5; :: thesis: verum