theorem Th1: :: PROCAL_1:1

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