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

A1: 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;

now :: thesis: ( r is Integer implies ( [\r/] = r & r = [/r\] & [\r/] = [/r\] ) )

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

end;

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