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