let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A holds p 'or' q = ('not' p) => q
let p, q be Element of CQC-WFF A; :: thesis: p 'or' q = ('not' p) => q
('not' p) => q = 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def 2;
hence p 'or' q = ('not' p) => q by QC_LANG2:def 3; :: thesis: verum