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 Th153
.= (variables_in H1) \/ (variables_in ('not' H2)) by Th154
.= (variables_in H1) \/ (variables_in H2) by Th153 ; :: thesis: verum