let p, q be Element of CQC-WFF ; :: 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