let a, b, c be positive Real; ( (a * b) * c = 1 implies ((1 / a) + (1 / b)) + (1 / c) >= ((sqrt a) + (sqrt b)) + (sqrt c) )
assume A1:
(a * b) * c = 1
; ((1 / a) + (1 / b)) + (1 / c) >= ((sqrt a) + (sqrt b)) + (sqrt c)
((1 / a) + (1 / b)) / 2 >= sqrt ((1 / a) * (1 / b))
by Th2;
then
((1 / a) + (1 / b)) / 2 >= sqrt (1 / (a * b))
by XCMPLX_1:102;
then A2:
((1 / a) + (1 / b)) / 2 >= sqrt ((1 * c) / ((a * b) * c))
by XCMPLX_1:91;
((1 / c) + (1 / a)) / 2 >= sqrt ((1 / c) * (1 / a))
by Th2;
then
((1 / c) + (1 / a)) / 2 >= sqrt (1 / (c * a))
by XCMPLX_1:102;
then A3:
((1 / c) + (1 / a)) / 2 >= sqrt ((1 * b) / ((c * a) * b))
by XCMPLX_1:91;
((1 / b) + (1 / c)) / 2 >= sqrt ((1 / b) * (1 / c))
by Th2;
then
((1 / b) + (1 / c)) / 2 >= sqrt (1 / (b * c))
by XCMPLX_1:102;
then
((1 / b) + (1 / c)) / 2 >= sqrt ((1 * a) / ((b * c) * a))
by XCMPLX_1:91;
then
(((1 / b) + (1 / c)) / 2) + (((1 / c) + (1 / a)) / 2) >= (sqrt a) + (sqrt b)
by A1, A3, XREAL_1:7;
then
((((1 / b) + (1 / c)) / 2) + (((1 / c) + (1 / a)) / 2)) + (((1 / a) + (1 / b)) / 2) >= ((sqrt a) + (sqrt b)) + (sqrt c)
by A1, A2, XREAL_1:7;
hence
((1 / a) + (1 / b)) + (1 / c) >= ((sqrt a) + (sqrt b)) + (sqrt c)
; verum