let p, q be Element of CQC-WFF ; :: thesis: p => (('not' p) => q) is valid
p => (('not' p) => q) in TAUT by Def1, Th76;
hence p => (('not' p) => q) is valid by Lm13; :: thesis: verum