let r be Real; :: thesis: ( [\r/] - 1 < r & [\r/] < r + 1 )
[\r/] <= r by Def6;
then A1: [\r/] + 0 < r + 1 by XREAL_1:8;
then [\r/] + (- 1) < (r + 1) + (- 1) by XREAL_1:6;
hence ( [\r/] - 1 < r & [\r/] < r + 1 ) by A1; :: thesis: verum