theorem :: QC_LANG3:27

for A being QC-alphabet
for p, q being QC-formula of A holds
( ( p is closed & q is closed ) iff p <=> q is closed )