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