theorem :: ASYMPT_1:84

ex N being Element of NAT st
for n being Element of NAT st n >= N holds
n - ((sqrt n) * (log (2,n))) > n / 2 by Lm40;