let r, s be Real; :: thesis: ( abs (r - s) = 1 iff ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) )
thus ( not abs (r - s) = 1 or ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) :: thesis: ( ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) implies abs (r - s) = 1 )

proof

assume A1: abs (r - s) = 1 ; :: thesis: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) )

now

per cases ( r > s or r = s or r < s ) by XXREAL_0:1;

case A2: r > s ; :: thesis: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) )

then 0 < r - s by XREAL_1:52;
then r - s = 1 by A1, ABSVALUE:def 1;
hence ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) by A2; :: thesis: verum

end;

case r = s ; :: thesis: contradiction

hence contradiction by A1, ABSVALUE:7; :: thesis: verum

end;

case A3: r < s ; :: thesis: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) )

then A4: 0 < s - r by XREAL_1:52;
1 = abs (- (r - s)) by A1, COMPLEX1:138
.= s - r by A4, ABSVALUE:def 1 ;
hence ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) by A3; :: thesis: verum

end;

end;

end;

hence ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) ; :: thesis: verum

end;

assume A5: ( ( r > s & r = s + 1 ) or ( r < s & s = r + 1 ) ) ; :: thesis: abs (r - s) = 1

per cases ( ( r > s & r = s + 1 ) or ( s > r & s = r + 1 ) ) by A5;

suppose ( r > s & r = s + 1 ) ; :: thesis: abs (r - s) = 1

hence abs (r - s) = 1 by ABSVALUE:def 1; :: thesis: verum

end;

suppose A6: ( s > r & s = r + 1 ) ; :: thesis: abs (r - s) = 1

thus abs (r - s) = abs (- (r - s)) by COMPLEX1:138
.= 1 by A6, ABSVALUE:def 1 ; :: thesis: verum

end;

end;