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 Def5;
hence r < [/r\] by A1, XXREAL_0:1; :: thesis: verum

end;

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