theorem Th9: :: PRE_FF:9

for r, s being Real st r >= s holds
[\r/] >= [\s/]