theorem :: ZF_LANG1:145

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