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 = {} & ( for M being non empty set holds
( M |= S iff M |= H ) ) ) by Th6;
( ( M1 |= S implies M2 |= S ) & ( M2 |= S implies M1 |= S ) & ( M1 |= S implies M1 |= H ) & ( M1 |= H implies M1 |= S ) & ( M2 |= S implies M2 |= H ) & ( M2 |= H implies M2 |= S ) ) by A1, A2;
hence ( M1 |= H iff M2 |= H ) ; :: thesis: verum

end;

assume A3: 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 A3; :: thesis: verum