let p be QC-formula; :: 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 29 :: thesis: 'not' p is closed
hence still_not-bound_in ('not' p) = {} by Th11; :: according to QC_LANG1:def 29 :: thesis: verum

end;

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