let p, q be QC-formula; :: thesis: ( ( p is closed & q is closed ) iff p '&' q is closed )
thus ( p is closed & q is closed implies p '&' q is closed ) :: thesis: ( p '&' q is closed implies ( p is closed & q is closed ) )

proof

assume ( still_not-bound_in p = {} & still_not-bound_in q = {} ) ; :: according to QC_LANG1:def 29 :: thesis: p '&' q is closed
then (still_not-bound_in p) \/ (still_not-bound_in q) = {} ;
hence still_not-bound_in (p '&' q) = {} by Th14; :: according to QC_LANG1:def 29 :: thesis: verum

end;

assume A1: still_not-bound_in (p '&' q) = {} ; :: according to QC_LANG1:def 29 :: thesis: ( p is closed & q is closed )
still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by Th14;
hence ( still_not-bound_in p = {} & still_not-bound_in q = {} ) by A1, XBOOLE_1:15; :: according to QC_LANG1:def 29 :: thesis: verum