let a, b, c be positive Real; ((((b + c) - a) / a) + (((c + a) - b) / b)) + (((a + b) - c) / c) >= 3
A1:
((b / a) + (c / b)) + (a / c) >= 3
by Th20;
((a / b) + (b / c)) + (c / a) >= 3
by Th20;
then
(((a / b) + (b / c)) + (c / a)) + (((b / a) + (c / b)) + (a / c)) >= 3 + 3
by A1, XREAL_1:7;
then A2:
((((((a / b) + (b / c)) + (c / a)) + (b / a)) + (c / b)) + (a / c)) - 3 >= 6 - 3
by XREAL_1:9;
((((b + c) - a) / a) + (((c + a) - b) / b)) + (((a + b) - c) / c) =
((((b + c) / a) - (a / a)) + (((c + a) - b) / b)) + (((a + b) - c) / c)
by XCMPLX_1:120
.=
((((b + c) / a) - 1) + (((c + a) - b) / b)) + (((a + b) - c) / c)
by XCMPLX_1:60
.=
((((b + c) / a) - 1) + (((c + a) / b) - (b / b))) + (((a + b) - c) / c)
by XCMPLX_1:120
.=
((((b + c) / a) - 1) + (((c + a) / b) - 1)) + (((a + b) - c) / c)
by XCMPLX_1:60
.=
(((((b + c) / a) - 1) + ((c + a) / b)) - 1) + (((a + b) / c) - (c / c))
by XCMPLX_1:120
.=
(((((b + c) / a) - 1) + ((c + a) / b)) - 1) + (((a + b) / c) - 1)
by XCMPLX_1:60
.=
((((b + c) / a) + ((c + a) / b)) + ((a + b) / c)) - 3
.=
((((b / a) + (c / a)) + ((c + a) / b)) + ((a + b) / c)) - 3
by XCMPLX_1:62
.=
((((b / a) + (c / a)) + ((c / b) + (a / b))) + ((a + b) / c)) - 3
by XCMPLX_1:62
.=
((((b / a) + (c / a)) + ((c / b) + (a / b))) + ((a / c) + (b / c))) - 3
by XCMPLX_1:62
.=
((((((a / b) + (b / c)) + (c / a)) + (b / a)) + (c / b)) + (a / c)) - 3
;
hence
((((b + c) - a) / a) + (((c + a) - b) / b)) + (((a + b) - c) / c) >= 3
by A2; verum