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