let r be real number ; :: thesis: r < [\r/] + 1
r - 1 < [\r/] by Def6;
then (r - 1) + 1 < [\r/] + 1 by XREAL_1:6;
hence r < [\r/] + 1 ; :: thesis: verum