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