let p, q be Element of CQC-WFF ; :: thesis: ( p => q in TAUT iff ('not' q) => ('not' p) in TAUT )
(p => q) => (('not' q) => ('not' p)) in TAUT by Th26;
hence ( p => q in TAUT implies ('not' q) => ('not' p) in TAUT ) by CQC_THE1:46; :: thesis: ( ('not' q) => ('not' p) in TAUT implies p => q in TAUT )
(('not' q) => ('not' p)) => (p => q) in TAUT by Th24;
hence ( ('not' q) => ('not' p) in TAUT implies p => q in TAUT ) by CQC_THE1:46; :: thesis: verum