theorem :: ASYMPT_1:47

for n being Element of NAT st n >= 30 holds
2 to_power n > n to_power 6 by Lm30;