theorem :: CQC_THE1:42

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