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 Th60
.= (Free ('not' p)) \ {x} by Th62
.= (Free p) \ {x} by Th60 ; :: thesis: verum