let a, r be Real; :: 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 [\a/] = [\r/] by A1, Th65;
hence frac r <= frac a by A1, XREAL_1:9; :: thesis: verum