theorem :: ASYMPT_1:48

for x being Real st x > 9 holds
2 to_power x > (2 * x) ^2 by Lm31;