for e being Real st 0 < e & e < 1 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
(n * (log (2,(1 + e)))) - (8 * (log (2,n))) > 8 * (log (2,n)) by Lm25;