let r1, r2, s be Real; :: thesis: ( 0 < s & r1 <= r2 implies ( r1 < r2 + s & r1 - s < r2 ) )
assume A1: 0 < s ; :: thesis: ( not r1 <= r2 or ( r1 < r2 + s & r1 - s < r2 ) )
assume r1 <= r2 ; :: thesis: ( r1 < r2 + s & r1 - s < r2 )
then r1 + 0 < r2 + s by A1, XREAL_1:8;
hence ( r1 < r2 + s & r1 - s < r2 ) by XREAL_1:19; :: thesis: verum