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