let r be real number ; :: thesis: ( frac r < 1 & 0 <= frac r )
A1: ( r - 1 < [\r/] & [\r/] <= 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 A2: ((frac r) - 1) + 1 < 0 + 1 by XREAL_1:8;
[\r/] + (r - [\r/]) <= r + (frac r) by A1, XREAL_1:8;
then r - r <= (r + (frac r)) - r by XREAL_1:11;
hence ( frac r < 1 & 0 <= frac r ) by A2; :: thesis: verum