theorem :: PROCAL_1:13

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