theorem :: ASYMPT_1:89

for n being Element of NAT st n >= 4 holds
n * (log (2,n)) >= 2 * n by Lm45;