theorem :: QC_LANG3:25

for A being QC-alphabet
for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p 'or' q is closed )