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