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