for n being Element of NAT st n >= 3 holds
n ^2 > (2 * n) + 1 by Lm27;