theorem Th147: :: ZF_LANG1:147

for H being ZF-formula
for x, y being Variable holds variables_in (All (x,y,H)) = (variables_in H) \/ {x,y}