theorem Th2: :: PROCAL_1:2

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