let g, h, i be Integer; :: thesis: ( g <= h + i & h < 0 & i < 0 implies ( g < h & g < i ) )
assume A1: ( g <= h + i & h < 0 & i < 0 ) ; :: thesis: ( g < h & g < i )
then g - i <= (h + i) - i by XREAL_1:11;
then i + (g + (- i)) < 0 + h by A1, XREAL_1:10;
hence g < h ; :: thesis: g < i
g - h <= (i + h) - h by A1, XREAL_1:11;
then h + (g + (- h)) < 0 + i by A1, XREAL_1:10;
hence g < i ; :: thesis: verum