let p, q be QC-formula; :: thesis: ( ( p is closed & q is closed ) iff p 'or' q is closed )
p 'or' q = 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def 3;
then ( ( p 'or' q is closed implies ('not' p) '&' ('not' q) is closed ) & ( ('not' p) '&' ('not' q) is closed implies p 'or' q is closed ) & ( ('not' p) '&' ('not' q) is closed implies ( 'not' p is closed & 'not' q is closed ) ) & ( 'not' p is closed & 'not' q is closed implies ('not' p) '&' ('not' q) is closed ) & ( 'not' p is closed implies p is closed ) & ( p is closed implies 'not' p is closed ) & ( 'not' q is closed implies q is closed ) & ( q is closed implies 'not' q is closed ) ) by Th25, Th26;
hence ( ( p is closed & q is closed ) iff p 'or' q is closed ) ; :: thesis: verum