theorem Th21: :: QC_LANG3:21

for A being QC-alphabet
for p being QC-formula of A holds
( p is closed iff 'not' p is closed ) by Th7;