let a, r be real number ; :: thesis: ( a >= [\r/] + 1 & a < r + 1 implies frac a < frac r )
assume A1: a >= [\r/] + 1 ; :: thesis: ( not a < r + 1 or frac a < frac r )
assume A2: a < r + 1 ; :: thesis: frac a < frac r
then A3: [\a/] = [\r/] + 1 by A1, Th5;
A4: ( frac a = a - [\a/] & frac r = r - [\r/] ) by INT_1:def 6;
a - 1 < r by A2, XREAL_1:21;
then (a - 1) - [\r/] < r - [\r/] by XREAL_1:16;
hence frac a < frac r by A3, A4; :: thesis: verum