let p, q be Element of CQC-WFF ; :: thesis: p => (p 'or' q) in TAUT
p => (('not' p) => q) in TAUT by CQC_THE1:79;
hence p => (p 'or' q) in TAUT by Lm1; :: thesis: verum