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