theorem Th69: :: INT_1:71

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