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 Th159
.= ((variables_in H) \/ {y,z}) \/ {x} by Th161
.= (variables_in H) \/ ({y,z} \/ {x}) by XBOOLE_1:4
.= (variables_in H) \/ {y,z,x} by ENUMSET1:43
.= (variables_in H) \/ {x,y,z} by ENUMSET1:100 ; :: thesis: verum