:: deftheorem defines <==> ZFREFLE1:def 2 :
for M1, M2 being non empty set holds
( M1 <==> M2 iff for H being ZF-formula st Free H = {} holds
( M1 |= H iff M2 |= H ) );