theorem :: ZF_LANG1:143

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