theorem Th28: :: INT_1:28

for r being Real
for i0 being Integer holds [\r/] + i0 = [\(r + i0)/]