let p be Element of CQC-WFF ; :: thesis: ('not' p) 'or' p in TAUT
(p 'or' ('not' p)) => (('not' p) 'or' p) in TAUT by Th8;
hence ('not' p) 'or' p in TAUT by Th2, CQC_THE1:82; :: thesis: verum