let p, q be boolean object ; :: thesis: (p => q) => (('not' q) => ('not' p)) = TRUE
A1: ( p = TRUE or p = FALSE ) by XBOOLEAN:def 3;
( q = TRUE or q = FALSE ) by XBOOLEAN:def 3;
hence (p => q) => (('not' q) => ('not' p)) = TRUE by A1; :: thesis: verum