theorem Th15: :: SERIES_3:15
for a, b, c being positive Real holds (a + b) + c >= 3 * (3 -root ((a * b) * c))