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