theorem Th21: :: DIOPHAN2:17

for a being Real
for n being Integer st a is not Integer & ( n = [\a/] or n = [\a/] + 1 ) holds
|.(a - n).| < 1