theorem Th81: :: ZF_LANG1:81

for x being Variable
for M being non empty set holds
( not M |= x 'in' x & M |= 'not' (x 'in' x) )