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 Th140
.= (variables_in ('not' H)) \/ {x} by Th142
.= (variables_in H) \/ {x} by Th140 ; :: thesis: verum