let r be real number ; :: thesis: ( [\r/] < r iff not r is integer )

now

assume A1: r is not Integer ; :: thesis: [\r/] < r
[\r/] <= r by Def6;
hence [\r/] < r by A1, XXREAL_0:1; :: thesis: verum

end;

hence ( [\r/] < r iff not r is integer ) by Th47; :: thesis: verum