theorem Th79: :: ZF_LANG1:79

for x being Variable
for M being non empty set holds M |= x '=' x by Th78;