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