let r be real number ; :: thesis: ( [/r\] = r iff r is integer )
r + 0 < r + 1 by XREAL_1:6;
hence ( [/r\] = r iff r is integer ) by Def5; :: thesis: verum