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