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