let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds (p 'or' q) => (('not' p) => q) is valid
let p, q be Element of CQC-WFF A; :: thesis: (p 'or' q) => (('not' p) => q) is valid
thus (p 'or' q) => (('not' p) => q) in TAUT A by PROCAL_1:5; :: according to CQC_THE1:def 10 :: thesis: verum