let A be QC-alphabet ; :: thesis: for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p '&' q is closed )
let p, q be QC-formula of A; :: 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 31 :: thesis: p '&' q is closed
then (still_not-bound_in p) \/ (still_not-bound_in q) = {} ;
hence still_not-bound_in (p '&' q) = {} by Th10; :: according to QC_LANG1:def 31 :: thesis: verum
end;
assume A1: still_not-bound_in (p '&' q) = {} ; :: according to QC_LANG1:def 31 :: thesis: ( p is closed & q is closed )
still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q) by Th10;
hence ( still_not-bound_in p = {} & still_not-bound_in q = {} ) by A1, XBOOLE_1:15; :: according to QC_LANG1:def 31 :: thesis: verum