theorem Th148: :: ZF_LANG1:148

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