theorem :: PROCAL_1:9

for A being QC-alphabet
for p being Element of CQC-WFF A holds ('not' p) 'or' p in TAUT A