let r be real number ; :: thesis: ( [\r/] - 1 < r & [\r/] < r + 1 )
[\r/] <= r by Def4;
then A1: [\r/] + 0 < r + 1 by XREAL_1:10;
then [\r/] + (- 1) < (r + 1) + (- 1) by XREAL_1:8;
hence ( [\r/] - 1 < r & [\r/] < r + 1 ) by A1; :: thesis: verum