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