a + b > a + 0 by XREAL_1:6;
then (a + b) / a > (1 * a) / a by XREAL_1:74;
hence (a + b) / a is heavy by XCMPLX_1:89; :: thesis: verum