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