theorem Th80: :: ZF_LANG:80

for x, y being Variable holds Subformulae (x '=' y) = {(x '=' y)}