theorem Th65: :: INT_1:67

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