theorem :: COMPLEX3:18
for a, b, c being positive Real st a < b holds
(b + c) / (a + c) is heavy by SERIES_5:3;