let r be real number ; :: thesis: ( [\r/] = [/r\] iff not [\r/] + 1 = [/r\] )
set Diff = [/r\] + (- [\r/]);

A1: now

assume r is Integer ; :: thesis: ( [\r/] = [/r\] & [\r/] + 1 <> [/r\] )
then [\r/] = [/r\] by Th59;
hence ( [\r/] = [/r\] & [\r/] + 1 <> [/r\] ) ; :: thesis: verum

end;

now

assume r is not Integer ; :: thesis: ( [\r/] + 1 = [/r\] & [\r/] <> [/r\] )
then [\r/] < [/r\] by Th60;
then [\r/] + (- [\r/]) < [/r\] + (- [\r/]) by XREAL_1:8;
then A2: 1 <= [/r\] + (- [\r/]) by Lm5;
A3: [/r\] < r + 1 by Def5;
r - 1 < [\r/] by Def4;
then - [\r/] < - (r - 1) by XREAL_1:26;
then [/r\] + (- [\r/]) < (r + 1) + (- (r - 1)) by A3, XREAL_1:10;
then (([/r\] + (- [\r/])) + 1) + (- 1) <= (1 + 1) + (- 1) by Th20;
then [\r/] + 1 = [\r/] + ([/r\] + (- [\r/])) by A2, XXREAL_0:1;
hence ( [\r/] + 1 = [/r\] & [\r/] <> [/r\] ) ; :: thesis: verum

end;

hence ( [\r/] = [/r\] iff not [\r/] + 1 = [/r\] ) by A1; :: thesis: verum