theorem Th139: :: ZF_LANG1:139

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