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