let A be QC-alphabet ; :: thesis: for p being QC-formula of A holds
( p is closed iff 'not' p is closed )
let p be QC-formula of A; :: thesis: ( p is closed iff 'not' p is closed )
thus ( p is closed implies 'not' p is closed ) :: thesis: ( 'not' p is closed implies p is closed )

proof

assume still_not-bound_in p = {} ; :: according to QC_LANG1:def 31 :: thesis: 'not' p is closed
hence still_not-bound_in ('not' p) = {} by Th7; :: according to QC_LANG1:def 31 :: thesis: verum

end;

assume still_not-bound_in ('not' p) = {} ; :: according to QC_LANG1:def 31 :: thesis: p is closed
hence still_not-bound_in p = {} by Th7; :: according to QC_LANG1:def 31 :: thesis: verum