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