let H1, H2 be ZF-formula; :: thesis: variables_in (H1 'or' H2) = (variables_in H1) \/ (variables_in H2)
thus variables_in (H1 'or' H2) = variables_in (('not' H1) '&' ('not' H2)) by Th140
.= (variables_in ('not' H1)) \/ (variables_in ('not' H2)) by Th141
.= (variables_in H1) \/ (variables_in ('not' H2)) by Th140
.= (variables_in H1) \/ (variables_in H2) by Th140 ; :: thesis: verum