theorem :: SERIES_5:6

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