let a, b, c be positive Real; :: thesis: (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (c ^2)
(((b * c) / a) ^2) + (((c * a) / b) ^2) >= (2 * ((b * c) / a)) * ((c * a) / b) by SERIES_3:6;
then (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (((b * c) / a) * ((c * a) / b)) ;
then (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (((b * c) * (c * a)) / (a * b)) by XCMPLX_1:76;
then (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (((b * a) * (c * c)) / ((a * b) * 1)) ;
then (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * ((c * c) / 1) by XCMPLX_1:91;
hence (((b * c) / a) ^2) + (((c * a) / b) ^2) >= 2 * (c ^2) ; :: thesis: verum