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