let a, b, c be positive Real; :: thesis: ((a / b) + (b / c)) + (c / a) >= 3
((a / b) + (b / c)) + (c / a) >= 3 * (3 -root (((a / b) * (b / c)) * (c / a))) by SERIES_3:15;
then ((a / b) + (b / c)) + (c / a) >= 3 * (3 -root (((a * b) / (b * c)) * (c / a))) by XCMPLX_1:76;
then ((a / b) + (b / c)) + (c / a) >= 3 * (3 -root ((a / c) * (c / a))) by XCMPLX_1:91;
then ((a / b) + (b / c)) + (c / a) >= 3 * (3 -root ((a * c) / (c * a))) by XCMPLX_1:76;
then ((a / b) + (b / c)) + (c / a) >= 3 * (3 -root 1) by XCMPLX_1:60;
then ((a / b) + (b / c)) + (c / a) >= 3 * 1 by POWER:6;
hence ((a / b) + (b / c)) + (c / a) >= 3 ; :: thesis: verum