theorem :: ASYMPT_1:45

for n being Element of NAT st n >= 10 holds
2 to_power (n - 1) > (2 * n) ^2 by Lm28;