let r be Real; :: thesis: ( r - 1 < [/r\] & r < [/r\] + 1 )
r <= [/r\] by Def7;
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