theorem :: CQC_THE1:43

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al holds p => (('not' p) => q) in TAUT Al