theorem :: SERIES_5:18
for a, b, c, d being positive Real holds sqrt ((a + b) * (c + d)) >= (sqrt (a * c)) + (sqrt (b * d))