(a + b) / a is heavy ;
then (a / (a + b)) " is heavy by XCMPLX_1:213;
hence a / (a + b) is light ; :: thesis: verum