theorem Th142: :: ZF_LANG1:142

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