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