theorem Th58: :: ZF_LANG1:58

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