theorem Th80: :: ZF_LANG1:80

for x being Variable
for M being non empty set
for v being Function of VAR,M holds not M,v |= x 'in' x