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

now

assume r is not Integer ; :: thesis: [\r/] < [/r\]
then ( [\r/] < r & r < [/r\] ) by Th48, Th55;
hence [\r/] < [/r\] by XXREAL_0:2; :: thesis: verum

end;

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