let r1, r2 be Real; :: thesis: ( r1 <= r2 - 1 implies [\r1/] <= [\r2/] - 1 )
( r1 <= r2 - 1 implies [\r1/] <= [\r2/] - 1 )
proof
assume r1 <= r2 - 1 ; :: thesis: [\r1/] <= [\r2/] - 1
then r1 + 1 <= (r2 - 1) + 1 by XREAL_1:6;
then [\(r1 + 1)/] <= [\r2/] by Lm4;
then [\r1/] + 1 <= [\r2/] by INT_1:28;
then ([\r1/] + 1) - 1 <= [\r2/] - 1 by XREAL_1:9;
hence [\r1/] <= [\r2/] - 1 ; :: thesis: verum
end;
hence ( r1 <= r2 - 1 implies [\r1/] <= [\r2/] - 1 ) ; :: thesis: verum