let q, p be Element of CQC-WFF ; :: thesis: (q => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT
A1: ( (('not' p) => p) => p in TAUT & (('not' ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT ) by CQC_THE1:78;
((('not' p) => p) => p) => (((('not' ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => ((q => ((('not' p) => p) => p)) => ((('not' p) => p) => p))) in TAUT by Lm6;
then ((('not' ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => ((q => ((('not' p) => p) => p)) => ((('not' p) => p) => p)) in TAUT by A1, CQC_THE1:82;
hence (q => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT by A1, CQC_THE1:82; :: thesis: verum