theorem :: ASYMPT_2:14

for x being Nat st 1 < x holds
ex N being Nat st
for n being Nat st N <= n holds
4 < n / (log (x,n))