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;
hence ( r is Integer implies [/r\] = r ) by Def5; :: thesis: verum

end;

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