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