theorem PP1: :: COMPLEX3:19

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