let r be Real; :: thesis: ( [\r/] = [/r\] iff r is integer )

now :: thesis: ( r is not Integer implies [\r/] <> [/r\] )

assume A2: r is not Integer ; :: thesis: [\r/] <> [/r\]
then [\r/] < r by Th26;
hence [\r/] <> [/r\] by A2, Th31; :: thesis: verum

end;

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