let a, b, c be positive Real; :: thesis: ( (a + b) + c = 1 implies (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8 )
A1: (a + c) / b >= (2 * (sqrt (a * c))) / b by SIN_COS2:1, XREAL_1:72;
A2: (a + b) / c >= (2 * (sqrt (a * b))) / c by SIN_COS2:1, XREAL_1:72;
A3: sqrt (a * b) > 0 by SQUARE_1:25;
A4: sqrt (a * c) > 0 by SQUARE_1:25;
assume A5: (a + b) + c = 1 ; :: thesis: (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8
then A6: (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) = (((b + c) / a) * ((1 / b) - 1)) * ((1 / c) - 1) by Lm17
.= (((b + c) / a) * ((a + c) / b)) * ((1 / c) - 1) by A5, Lm17
.= (((b + c) / a) * ((a + c) / b)) * ((((a + b) / c) + (c / c)) - 1) by A5, XCMPLX_1:62
.= (((b + c) / a) * ((a + c) / b)) * ((((a + b) / c) + 1) - 1) by XCMPLX_1:60
.= (((b + c) / a) * ((a + c) / b)) * ((a + b) / c) ;
A7: sqrt (b * c) > 0 by SQUARE_1:25;
(b + c) / a >= (2 * (sqrt (b * c))) / a by SIN_COS2:1, XREAL_1:72;
then ((b + c) / a) * ((a + c) / b) >= ((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b) by A1, A7, A4, XREAL_1:66;
then (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= (((2 * (sqrt (b * c))) / a) * ((2 * (sqrt (a * c))) / b)) * ((2 * (sqrt (a * b))) / c) by A6, A2, A7, A4, A3, XREAL_1:66;
hence (((1 / a) - 1) * ((1 / b) - 1)) * ((1 / c) - 1) >= 8 by Lm18; :: thesis: verum