theorem :: ASYMPT_1:61

for n being Element of NAT st n >= 2 holds
2 to_power n > n + 1 by Lm1;