( a <= 1 & b < - 1 ) by TA1;
then a + b < 1 + (- 1) by XREAL_1:8;
then a + b < 0 ;
hence a + b is negative ; :: thesis: verum