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