theorem Th5: :: SERIES_5:5
for a, b being positive Real st a < b holds
sqrt (a / b) < (b + (sqrt (((a ^2) + (b ^2)) / 2))) / (a + (sqrt (((a ^2) + (b ^2)) / 2)))