let p, q be Element of CQC-WFF ; :: thesis: ( ('not' p) => q in TAUT implies ('not' q) => p in TAUT )
assume A1: ('not' p) => q in TAUT ; :: thesis: ('not' q) => p in TAUT
(('not' p) => q) => (('not' q) => p) in TAUT by Th31;
hence ('not' q) => p in TAUT by A1, CQC_THE1:82; :: thesis: verum