theorem :: NEWTON02:57

for b being Nat st b > 0 holds
ex n being Nat st
( b >= 2 |^ n & b < 2 |^ (n + 1) )