theorem Th66: :: INT_1:68

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