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