let H be ZF-formula; :: thesis: for x being Variable holds variables_in (Ex (x,H)) = (variables_in H) \/ {x}
let x be Variable; :: thesis: variables_in (Ex (x,H)) = (variables_in H) \/ {x}
thus variables_in (Ex (x,H)) = variables_in (All (x,('not' H))) by Th153
.= (variables_in ('not' H)) \/ {x} by Th155
.= (variables_in H) \/ {x} by Th153 ; :: thesis: verum