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

end;

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