let r, s be Real; :: thesis: ( r >= s implies [\r/] >= [\s/] )
assume A1: r >= s ; :: thesis: [\r/] >= [\s/]
A2: [\s/] <= s by INT_1:def 6;
r - 1 < [\r/] by INT_1:def 6;
then A3: (r - 1) + 1 < [\r/] + 1 by XREAL_1:6;
assume [\r/] < [\s/] ; :: thesis: contradiction
then [\r/] + 1 <= [\s/] by INT_1:7;
then r < [\s/] by A3, XXREAL_0:2;
hence contradiction by A1, A2, XXREAL_0:2; :: thesis: verum