let a, r be Real; :: thesis: ( r <= a & a < [\r/] + 1 implies [\a/] = [\r/] )
assume A1: r <= a ; :: thesis: ( not a < [\r/] + 1 or [\a/] = [\r/] )
assume a < [\r/] + 1 ; :: thesis: [\a/] = [\r/]
then A2: a - 1 < ([\r/] + 1) - 1 by XREAL_1:9;
[\r/] <= r by Def6;
then [\r/] <= a by A1, XXREAL_0:2;
hence [\a/] = [\r/] by A2, Def6; :: thesis: verum