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