theorem :: CQC_THE1:61

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