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