let M1, M2 be non empty set ; :: thesis: ( M1 <==> M2 iff for H being ZF-formula holds
( M1 |= H iff M2 |= H ) )
thus ( M1 <==> M2 implies for H being ZF-formula holds
( M1 |= H iff M2 |= H ) ) :: thesis: ( ( for H being ZF-formula holds
( M1 |= H iff M2 |= H ) ) implies M1 <==> M2 )

proof

assume A1: for H being ZF-formula st Free H = {} holds
( M1 |= H iff M2 |= H ) ; :: according to ZFREFLE1:def 2 :: thesis: for H being ZF-formula holds
( M1 |= H iff M2 |= H )
let H be ZF-formula; :: thesis: ( M1 |= H iff M2 |= H )
consider S being ZF-formula such that
A2: Free S = {} and
A3: for M being non empty set holds
( M |= S iff M |= H ) by Th6;
( M1 |= S iff M2 |= S ) by A1, A2;
hence ( M1 |= H iff M2 |= H ) by A3; :: thesis: verum

end;

assume A4: for H being ZF-formula holds
( M1 |= H iff M2 |= H ) ; :: thesis: M1 <==> M2
let H be ZF-formula; :: according to ZFREFLE1:def 2 :: thesis: ( Free H = {} implies ( M1 |= H iff M2 |= H ) )
thus ( Free H = {} implies ( M1 |= H iff M2 |= H ) ) by A4; :: thesis: verum