theorem Th4: :: MESFUNC5:4

for n being Nat
for p being ExtReal st 0 <= p & p < n holds
ex k being Nat st
( 1 <= k & k <= (2 |^ n) * n & (k - 1) / (2 |^ n) <= p & p < k / (2 |^ n) )