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