theorem Th78: :: ZF_LANG1:78

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