let g, h, i be Integer; :: thesis: ( g <= h + i & h < 0 & i < 0 implies ( g < h & g < i ) )
assume that
A1: g <= h + i and
A2: h < 0 and
A3: i < 0 ; :: thesis: ( g < h & g < i )
g - i <= (h + i) - i by A1, XREAL_1:9;
then i + (g + (- i)) < 0 + h by A3, XREAL_1:8;
hence g < h ; :: thesis: g < i
g - h <= (i + h) - h by A1, XREAL_1:9;
then h + (g + (- h)) < 0 + i by A2, XREAL_1:8;
hence g < i ; :: thesis: verum