let q, p be Element of CQC-WFF ; :: thesis: (q => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT
( (('not' p) => p) => p in TAUT & ((('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, CQC_THE1:42;
then ( (('not' ((('not' p) => p) => p)) => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT & ((('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 CQC_THE1:42, CQC_THE1:46;
hence (q => ((('not' p) => p) => p)) => ((('not' p) => p) => p) in TAUT by CQC_THE1:46; :: thesis: verum