let p be Element of CQC-WFF ; :: thesis: p => p in TAUT
( (('not' p) => p) => p in TAUT & p => (('not' p) => p) in TAUT ) by CQC_THE1:78, CQC_THE1:79;
hence p => p in TAUT by Th3; :: thesis: verum