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