theorem :: ZF_LANG1:83

for x, y being Variable
for M being non empty set holds
( M |= 'not' (x 'in' y) iff ( x = y or for X being set st X in M holds
X misses M ) )