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