let a, b, c be positive Real; :: thesis: ( ((a * b) + (b * c)) + (c * a) = 1 implies (a + b) + c >= sqrt 3 )
assume A1: ((a * b) + (b * c)) + (c * a) = 1 ; :: thesis: (a + b) + c >= sqrt 3
then ((a ^2) + (b ^2)) + (c ^2) >= 1 by SERIES_3:10;
then (((a ^2) + (b ^2)) + (c ^2)) + 2 >= 1 + 2 by XREAL_1:6;
then sqrt (((a + b) + c) ^2) >= sqrt 3 by A1, SQUARE_1:26;
hence (a + b) + c >= sqrt 3 by SQUARE_1:22; :: thesis: verum