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