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
A3: (q 'or' p) => (('not' q) => p) in TAUT by Th5;
(p 'or' q) => (q 'or' p) in TAUT by Th8;
then (p 'or' q) => (('not' q) => p) in TAUT by A3, LUKASI_1:3;
then ('not' q) => p in TAUT by A1, CQC_THE1:82;
hence p in TAUT by A2, CQC_THE1:82; :: thesis: verum