theorem Th68: :: INT_1:70

for a, r being Real st a >= [\r/] + 1 & a <= r + 1 holds
[\a/] = [\r/] + 1