let b, c be positive Nat; :: thesis: c * (frac (1 / (b + c))) < 1
c * (frac (1 / (b + c))) = c / (b + c) by XCMPLX_1:99;
hence c * (frac (1 / (b + c))) < 1 by COMPLEX3:1; :: thesis: verum