let a, r be Real; :: 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 a - 1 < r by XREAL_1:19;
then A3: ( frac a = a - [\a/] & (a - 1) - [\r/] < r - [\r/] ) by XREAL_1:14;
[\a/] = [\r/] + 1 by A1, A2, Th68;
hence frac a < frac r by A3; :: thesis: verum