theorem :: ASYMPT_1:46

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