theorem :: SERIES_5:21
for a, b, c being positive Real st ((a * b) + (b * c)) + (c * a) = 1 holds
(a + b) + c >= sqrt 3