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 in TAUT & VERUM => (('not' ('not' p)) => p) in TAUT ) by Th15, CQC_THE1:77;
hence ('not' ('not' p)) => p in TAUT by CQC_THE1:82; :: thesis: verum