let p, q be Element of CQC-WFF ; :: thesis: ( (('not' ('not' p)) => q) => (p => q) in TAUT & (p => q) => (('not' ('not' p)) => q) in TAUT )
( (p => ('not' ('not' p))) => ((('not' ('not' p)) => q) => (p => q)) in TAUT & p => ('not' ('not' p)) in TAUT ) by Th1, Th27;
hence (('not' ('not' p)) => q) => (p => q) in TAUT by Th2; :: thesis: (p => q) => (('not' ('not' p)) => q) in TAUT
( (('not' ('not' p)) => p) => ((p => q) => (('not' ('not' p)) => q)) in TAUT & ('not' ('not' p)) => p in TAUT ) by Th1, Th25;
hence (p => q) => (('not' ('not' p)) => q) in TAUT by Th2; :: thesis: verum