( a >= - 1 & b >= 1 ) by TA1;
then a + b >= (- 1) + 1 by XREAL_1:7;
hence not a + b is negative ; :: thesis: verum