let s, r1, r2 be Real; :: thesis: ( not |.(r1 - r2).| > s or r1 + s < r2 or r2 + s < r1 )
assume A1: |.(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 |.(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 |.(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