theorem :: SERIES_5:12

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