theorem Th16: :: NIVEN:5

for r, t being Real st t > 0 holds
ex i being Integer st
( t * i <= r & r <= t * (i + 1) )