let p be ZF-formula; :: thesis: for x being Variable holds Free (Ex x,p) = (Free p) \ {x}
let x be Variable; :: thesis: Free (Ex x,p) = (Free p) \ {x}
thus Free (Ex x,p) = Free (All x,('not' p)) by Th65
.= (Free ('not' p)) \ {x} by Th67
.= (Free p) \ {x} by Th65 ; :: thesis: verum