theorem Th2: :: SERIES_3:2

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