let p be Element of CQC-WFF ; :: thesis: p => ('not' ('not' p)) in TAUT
( (VERUM => p) => (('not' p) => ('not' VERUM )) in TAUT & (('not' p) => ('not' VERUM )) => ('not' ('not' p)) in TAUT ) by Lm25, Th26;
then A1: (VERUM => p) => ('not' ('not' p)) in TAUT by Th3;
p => (VERUM => p) in TAUT by Th5;
hence p => ('not' ('not' p)) in TAUT by A1, Th3; :: thesis: verum