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