let p, q be Element of CQC-WFF ; :: thesis: ( p => ('not' q) is valid implies q => ('not' p) is valid )
assume A1: p => ('not' q) is valid ; :: thesis: q => ('not' p) is valid
(p => ('not' q)) => (q => ('not' p)) is valid by Th71;
hence q => ('not' p) is valid by A1, CQC_THE1:104; :: thesis: verum