theorem Th8: :: SERIES_5:8

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