let H be ZF-formula; :: thesis: for x, y being Variable holds variables_in (All (x,y,H)) = (variables_in H) \/ {x,y}
let x, y be Variable; :: thesis: variables_in (All (x,y,H)) = (variables_in H) \/ {x,y}
thus variables_in (All (x,y,H)) = (variables_in (All (y,H))) \/ {x} by Th142
.= ((variables_in H) \/ {y}) \/ {x} by Th142
.= (variables_in H) \/ ({y} \/ {x}) by XBOOLE_1:4
.= (variables_in H) \/ {x,y} by ENUMSET1:1 ; :: thesis: verum