let p be Element of CQC-WFF ; :: thesis: ('not' ('not' p)) => p in TAUT
( ('not' ('not' p)) => (('not' p) => ('not' VERUM)) in TAUT & (('not' p) => ('not' VERUM)) => (VERUM => p) in TAUT ) by Lm23, Th24;
then ('not' ('not' p)) => (VERUM => p) in TAUT by Th3;
then VERUM => (('not' ('not' p)) => p) in TAUT by Th15;
hence ('not' ('not' p)) => p in TAUT by CQC_THE1:77, CQC_THE1:82; :: thesis: verum