for r being Real holds
( [\r/] - 1 < r & [\r/] < r + 1 )