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 )
A2: ( frac a = a - [\a/] & frac r = r - [\r/] ) by INT_1:def 6;
assume a < [\r/] + 1 ; :: thesis: frac r <= frac a
then [\a/] = [\r/] by A1, Th2;
hence frac r <= frac a by A1, A2, XREAL_1:11; :: thesis: verum