theorem :: PROCAL_1:55

for A being QC-alphabet
for p, q being Element of CQC-WFF A st p 'or' q in TAUT A & 'not' q in TAUT A holds
p in TAUT A