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\]
then A2: r < [/r\] by Th31;
[\r/] < r by A1, Th26;
hence [\r/] < [/r\] by A2, XXREAL_0:2; :: thesis: verum

end;

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