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

proof

r + 0 < r + 1 by XREAL_1:6;
then r - 1 < (r + 1) - 1 by XREAL_1:9;
hence ( r is Integer implies [\r/] = r ) by Def6; :: thesis: verum

end;

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