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