let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds ('not' p) 'or' p in TAUT A
let p be Element of CQC-WFF A; :: thesis: ('not' p) 'or' p in TAUT A
(p 'or' ('not' p)) => (('not' p) 'or' p) in TAUT A by Th8;
hence ('not' p) 'or' p in TAUT A by Th2, CQC_THE1:46; :: thesis: verum