let p be Nat; :: thesis: ( p > 2 implies (2 * p) + 1 > 5 )
assume p > 2 ; :: thesis: (2 * p) + 1 > 5
then 2 * p > 2 * 2 by XREAL_1:68;
then (2 * p) + 1 > 4 + 1 by XREAL_1:8;
hence (2 * p) + 1 > 5 ; :: thesis: verum