a >= 1 by TA1;
then a + b > 1 + 0 by XREAL_1:8;
hence a + b is heavy ; :: thesis: verum