let r1, r2, s be Real; :: thesis: ( not abs (r1 - r2) > s or r1 + s < r2 or r2 + s < r1 )
assume A1: abs (r1 - r2) > s ; :: thesis: ( r1 + s < r2 or r2 + s < r1 )

now :: thesis: ( ( r1 < r2 & r1 + s < r2 ) or ( r2 <= r1 & r2 + s < r1 ) )

per cases ( r1 < r2 or r2 <= r1 ) ;

case r1 < r2 ; :: thesis: r1 + s < r2

then r1 - r2 < 0 by XREAL_1:49;
then abs (r1 - r2) = - (r1 - r2) by ABSVALUE:def 1
.= r2 - r1 ;
hence r1 + s < r2 by A1, XREAL_1:20; :: thesis: verum

end;

case r2 <= r1 ; :: thesis: r2 + s < r1

then r1 - r2 >= 0 by XREAL_1:48;
then abs (r1 - r2) = r1 - r2 by ABSVALUE:def 1;
hence r2 + s < r1 by A1, XREAL_1:20; :: thesis: verum

end;

end;

end;

hence ( r1 + s < r2 or r2 + s < r1 ) ; :: thesis: verum