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