theorem LMC31: :: ASYMPT_3:2

for r being Real ex N being Nat st
for n being Nat st N <= n holds
r < n / (log (2,n))