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

now :: thesis: ( r is not Integer implies [\r/] < r )

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 ) ; :: thesis: verum