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