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