theorem :: SERIES_5:11

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