let g, r, r1 be Real; :: thesis: ( 0 < g & r <= r1 implies ( r - g < r1 & r < r1 + g ) )
assume that
A1: 0 < g and
A2: r <= r1 ; :: thesis: ( r - g < r1 & r < r1 + g )
r - g < r1 - 0 by A1, A2, XREAL_1:15;
hence r - g < r1 ; :: thesis: r < r1 + g
r + 0 < r1 + g by A1, A2, XREAL_1:8;
hence r < r1 + g ; :: thesis: verum