let q, p be Element of CQC-WFF ; :: thesis: q => (p => q) in TAUT
A1: ( q => ((('not' p) => q) => q) in TAUT & p => (('not' p) => q) in TAUT ) by Lm12, CQC_THE1:79;
(q => ((('not' p) => q) => q)) => ((p => (('not' p) => q)) => (q => (p => q))) in TAUT by Lm2;
then (p => (('not' p) => q)) => (q => (p => q)) in TAUT by A1, CQC_THE1:82;
hence q => (p => q) in TAUT by A1, CQC_THE1:82; :: thesis: verum