theorem Th2: :: REAL_3:2

for i being Integer
for r being Real st i <= r & r < i + 1 holds
[\r/] = i