theorem :: SERIES_5:24
for a, b, c being positive Real holds (((b * c) / a) + ((a * c) / b)) + ((a * b) / c) >= (a + b) + c