let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds (('not' p) => q) => (p 'or' q) is valid
let p, q be Element of CQC-WFF A; :: thesis: (('not' p) => q) => (p 'or' q) is valid
('not' ('not' p)) => p in TAUT A by LUKASI_1:25;
then ( (('not' p) => q) => (('not' ('not' p)) 'or' q) in TAUT A & (('not' ('not' p)) 'or' q) => (p 'or' q) in TAUT A ) by PROCAL_1:14, PROCAL_1:48;
hence (('not' p) => q) => (p 'or' q) in TAUT A by LUKASI_1:3; :: according to CQC_THE1:def 10 :: thesis: verum