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 A1: r - 1 < (r + 1) - 1 by XREAL_1:9;
assume r is Integer ; :: thesis: [\r/] = r
hence [\r/] = r by A1, Def6; :: thesis: verum
end;
hence ( [\r/] = r iff r is integer ) ; :: thesis: verum