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