theorem Th10: :: SERIES_5:10
for a, b being positive Real holds 2 / ((1 / a) + (1 / b)) <= (a + b) / 2