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

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