for m, n being Element of NAT st m > 0 holds
ex i being Element of NAT st
( ( for k2 being Element of NAT st k2 < i holds
m * (2 |^ k2) <= n ) & m * (2 |^ i) > n )