theorem Th4: :: SERIES_5:4
for a, b being positive Real st a < b holds
a / b < sqrt (a / b)