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