let p, q be Element of CQC-WFF ; :: thesis: ( p 'or' q in TAUT & 'not' p in TAUT implies q in TAUT )
assume that
A1: p 'or' q in TAUT and
A2: 'not' p in TAUT ; :: thesis: q in TAUT
(p 'or' q) => (('not' p) => q) in TAUT by Th5;
then ('not' p) => q in TAUT by A1, CQC_THE1:46;
hence q in TAUT by A2, CQC_THE1:46; :: thesis: verum