let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds (p => ('not' p)) => ('not' p) in TAUT A
let p be Element of CQC-WFF A; :: thesis: (p => ('not' p)) => ('not' p) in TAUT A
( (('not' ('not' p)) => ('not' p)) => ('not' p) in TAUT A & (p => ('not' p)) => (('not' ('not' p)) => ('not' p)) in TAUT A ) by Th28, CQC_THE1:42;
hence (p => ('not' p)) => ('not' p) in TAUT A by Th3; :: thesis: verum