let x be bound_QC-variable; :: thesis: for p being QC-formula holds
( Ex x,p is closed iff still_not-bound_in p c= {x} )
let p be QC-formula; :: thesis: ( Ex x,p is closed iff still_not-bound_in p c= {x} )
thus ( Ex x,p is closed implies still_not-bound_in p c= {x} ) :: thesis: ( still_not-bound_in p c= {x} implies Ex x,p is closed )

proof

assume still_not-bound_in (Ex x,p) = {} ; :: according to QC_LANG1:def 30 :: thesis: still_not-bound_in p c= {x}
then {} = (still_not-bound_in p) \ {x} by Th23;
hence still_not-bound_in p c= {x} by XBOOLE_1:37; :: thesis: verum

end;

assume still_not-bound_in p c= {x} ; :: thesis: Ex x,p is closed
then {} = (still_not-bound_in p) \ {x} by XBOOLE_1:37;
hence still_not-bound_in (Ex x,p) = {} by Th23; :: according to QC_LANG1:def 30 :: thesis: verum