let p, q be Element of CQC-WFF ; :: thesis: (p => q) => (('not' q) => ('not' p)) in TAUT
A1: ('not' q) => ((p => ('not' VERUM )) => ('not' p)) in TAUT by Lm25, Th13;
A2: ('not' q) => (q => ('not' VERUM )) in TAUT by Lm23;
(q => ('not' VERUM )) => ((p => q) => (p => ('not' VERUM ))) in TAUT by Th9;
then ('not' q) => ((p => q) => (p => ('not' VERUM ))) in TAUT by A2, Th3;
then ('not' q) => ((p => q) => ('not' p)) in TAUT by A1, Th22;
hence (p => q) => (('not' q) => ('not' p)) in TAUT by Th15; :: thesis: verum