theorem :: ASYMPT_1:82

for n being Element of NAT st n >= 3 holds
2 * (n - 2) >= n - 1 by Lm35;