let A be QC-alphabet ; :: thesis: for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p 'or' q is closed )
let p, q be QC-formula of A; :: thesis: ( ( p is closed & q is closed ) iff p 'or' q is closed )
A1: p 'or' q = 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def 3;
( ('not' p) '&' ('not' q) is closed iff ( 'not' p is closed & 'not' q is closed ) ) by Th22;
hence ( ( p is closed & q is closed ) iff p 'or' q is closed ) by A1, Th21; :: thesis: verum