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