theorem :: ASYMPT_1:49

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