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