theorem Th7: :: SERIES_5:7

for a, b being positive Real holds 2 / ((1 / a) + (1 / b)) <= sqrt (a * b)