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