let n be Nat; :: thesis: ( 3 * n < ((n * n) + (3 * n)) + 1 & n < ((n * n) + (3 * n)) + 1 & 2 * n < ((n * n) + (3 * n)) + 1 )
3 * n <= (n * n) + (3 * n) by NAT_1:12;
hence A1: 3 * n < ((n * n) + (3 * n)) + 1 by NAT_1:13; :: thesis: ( n < ((n * n) + (3 * n)) + 1 & 2 * n < ((n * n) + (3 * n)) + 1 )
n <= 3 * n by Lm6;
hence n < ((n * n) + (3 * n)) + 1 by A1, XXREAL_0:2; :: thesis: 2 * n < ((n * n) + (3 * n)) + 1
2 * n <= 3 * n by NAT_1:4;
hence 2 * n < ((n * n) + (3 * n)) + 1 by A1, XXREAL_0:2; :: thesis: verum