theorem Th140: :: ZF_LANG1:140

for H being ZF-formula holds variables_in ('not' H) = variables_in H