let p, q be Element of CQC-WFF ; :: thesis: (p => q) => (('not' q) => ('not' p)) in TAUT
( ('not' q) => (q => ('not' VERUM)) in TAUT & (q => ('not' VERUM)) => ((p => q) => (p => ('not' VERUM))) in TAUT ) by Lm23, Th9;
then A1: ('not' q) => ((p => q) => (p => ('not' VERUM))) in TAUT by Th3;
('not' q) => ((p => ('not' VERUM)) => ('not' p)) in TAUT by Lm25, Th13;
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