theorem LMC31H1: :: ASYMPT_2:12

for x, y being Real st number_e < x & x <= y holds
x / (log (2,x)) <= y / (log (2,y))