let r1, r2 be Real; :: thesis: ( r1 <= r2 implies [\r1/] <= [\r2/] )
( r1 <= r2 implies [\r1/] <= [\r2/] )

proof

assume A1: r1 <= r2 ; :: thesis: [\r1/] <= [\r2/]

now :: thesis: not [\r2/] < [\r1/]

assume [\r2/] < [\r1/] ; :: thesis: contradiction
then A2: [\r2/] + 1 <= [\r1/] by INT_1:7;
[\r1/] <= r1 by INT_1:def 6;
then [\r2/] + 1 <= r1 by A2, XXREAL_0:2;
hence contradiction by A1, INT_1:29, XXREAL_0:2; :: thesis: verum

end;

hence [\r1/] <= [\r2/] ; :: thesis: verum

end;

hence ( r1 <= r2 implies [\r1/] <= [\r2/] ) ; :: thesis: verum