let i be Integer; :: thesis: for r being Real st i <= r holds
i <= [\r/]
let r be Real; :: thesis: ( i <= r implies i <= [\r/] )
assume i <= r ; :: thesis: i <= [\r/]
then A1: i - 1 <= r - 1 by XREAL_1:9;
r - 1 < [\r/] by Def6;
then i - 1 < [\r/] by A1, XXREAL_0:2;
then (i - 1) + 1 <= [\r/] by Th7;
hence i <= [\r/] ; :: thesis: verum