let r be real number ; :: thesis: ( [\r/] = r iff r is integer )
( r is Integer implies [\r/] = r )

proof

r + 0 < r + 1 by XREAL_1:8;
then A1: r - 1 < (r + 1) - 1 by XREAL_1:11;
assume r is Integer ; :: thesis: [\r/] = r
hence [\r/] = r by A1, Def4; :: thesis: verum

end;

hence ( [\r/] = r iff r is integer ) ; :: thesis: verum