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