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)) in TAUT by 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 in TAUT by Th25;
hence (p => q) => (('not' ('not' p)) => q) in TAUT by Th2; :: thesis: verum