for H1, H2 being ZF-formula holds variables_in (H1 => H2) = (variables_in H1) \/ (variables_in H2)