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