theorem :: INT_1:36

for r being Real holds [\r/] <= [/r\]