theorem Th26: :: QC_LANG3:26

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 )