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