theorem :: ASYMPT_1:66

for n being Element of NAT st n >= 6 holds
(n + 1) ^2 < 2 to_power n by Lm8;