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 => H2)) \/ (variables_in (H2 => H1)) by Th141
.= ((variables_in H1) \/ (variables_in H2)) \/ (variables_in (H2 => H1)) by Th144
.= ((variables_in H1) \/ (variables_in H2)) \/ ((variables_in H1) \/ (variables_in H2)) by Th144
.= (variables_in H1) \/ (variables_in H2) ; :: thesis: verum