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

A1: now

assume r is Integer ; :: thesis: ( [\r/] = r & r = [/r\] & [\r/] = [/r\] )
hence ( [\r/] = r & r = [/r\] ) by Th47, Th54; :: thesis: [\r/] = [/r\]
hence [\r/] = [/r\] ; :: thesis: verum

end;

now

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

end;

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