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