(b * 1) / (b * a) = 1 / a by XCMPLX_1:91;
hence b / (b * a) is positive ; :: thesis: verum