for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is closed & q is closed holds
( p |- q iff 'not' q |- 'not' p ) by Th43, Th45;