thus (p => q) => (('not' q) => ('not' p)) in TAUT by Th26; :: according to CQC_THE1:def 10 :: thesis: verum