let a, b, c be positive Real; :: thesis: ((((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) >= 6
sqrt (a * c) > 0 by SQUARE_1:25;
then A1: ((sqrt (a * c)) / b) + (b / (sqrt (a * c))) >= 2 by SERIES_3:3;
sqrt (b * c) > 0 by SQUARE_1:25;
then A2: (a / (sqrt (b * c))) + ((sqrt (b * c)) / a) >= 2 by SERIES_3:3;
sqrt (b * a) > 0 by SQUARE_1:25;
then ((sqrt (a * b)) / c) + (c / (sqrt (b * a))) >= 2 by SERIES_3:3;
then (((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + (((sqrt (a * b)) / c) + (c / (sqrt (b * a)))) >= 2 + 2 by A1, XREAL_1:7;
then (((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + ((a / (sqrt (b * c))) + ((sqrt (b * c)) / a)) >= 4 + 2 by A2, XREAL_1:7;
hence ((((((sqrt (a * c)) / b) + (b / (sqrt (a * c)))) + ((sqrt (a * b)) / c)) + (c / (sqrt (b * a)))) + (a / (sqrt (b * c)))) + ((sqrt (b * c)) / a) >= 6 ; :: thesis: verum