let i be Integer; :: thesis: for r being real number st i <= r holds
i <= [\r/]
let r be real number ; :: thesis: ( i <= r implies i <= [\r/] )
assume A1: i <= r ; :: thesis: i <= [\r/]
A2: r - 1 < [\r/] by Def4;
i - 1 <= r - 1 by A1, XREAL_1:11;
then i - 1 < [\r/] by A2, XXREAL_0:2;
then (i - 1) + 1 <= [\r/] by Th20;
hence i <= [\r/] ; :: thesis: verum