let b, c, a be real positive number ; :: thesis: ((((b + c) - a) / a) + (((c + a) - b) / b)) + (((a + b) - c) / c) >= 3
A1: ((((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:121
.= ((((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:121
.= ((((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:121
.= (((((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:63
.= ((((b / a) + (c / a)) + ((c / b) + (a / b))) + ((a + b) / c)) - 3 by XCMPLX_1:63
.= ((((b / a) + (c / a)) + ((c / b) + (a / b))) + ((a / c) + (b / c))) - 3 by XCMPLX_1:63
.= ((((((a / b) + (b / c)) + (c / a)) + (b / a)) + (c / b)) + (a / c)) - 3 ;
A2: ((a / b) + (b / c)) + (c / a) >= 3 by Th20;
((b / a) + (c / b)) + (a / c) >= 3 by Th20;
then (((a / b) + (b / c)) + (c / a)) + (((b / a) + (c / b)) + (a / c)) >= 3 + 3 by A2, XREAL_1:9;
then ((((((a / b) + (b / c)) + (c / a)) + (b / a)) + (c / b)) + (a / c)) - 3 >= 6 - 3 by XREAL_1:11;
hence ((((b + c) - a) / a) + (((c + a) - b) / b)) + (((a + b) - c) / c) >= 3 by A1; :: thesis: verum