let a, b, c be positive Real; ((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 = (((((c * a) / b) ^2) + (((a * b) / c) ^2)) + (((b * c) / a) ^2)) + (2 * (((a ^2) + (b ^2)) + (c ^2)))
((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 =
(((((b * c) / a) ^2) + (((c * a) / b) ^2)) + (((a * b) / c) ^2)) + ((((2 * ((b * c) / a)) * ((c * a) / b)) + ((2 * ((b * c) / a)) * ((a * b) / c))) + ((2 * ((c * a) / b)) * ((a * b) / c)))
.=
(((((b * c) / a) ^2) + (((c * a) / b) ^2)) + (((a * b) / c) ^2)) + (2 * (((a ^2) + (b ^2)) + (c ^2)))
by Lm15
;
hence
((((b * c) / a) + ((c * a) / b)) + ((a * b) / c)) ^2 = (((((c * a) / b) ^2) + (((a * b) / c) ^2)) + (((b * c) / a) ^2)) + (2 * (((a ^2) + (b ^2)) + (c ^2)))
; verum