theorem Th138: :: ZF_LANG1:138

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