let a, b, c, d be positive Real; (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) < 2
A1:
b / (a + b) > b / ((a + b) + c)
by XREAL_1:29, XREAL_1:76;
a / (a + b) > a / ((a + b) + d)
by XREAL_1:29, XREAL_1:76;
then
(a / (a + b)) + (b / (a + b)) > (a / ((a + b) + d)) + (b / ((a + b) + c))
by A1, XREAL_1:8;
then
(a + b) / (a + b) > (a / ((a + b) + d)) + (b / ((a + b) + c))
by XCMPLX_1:62;
then A2:
1 > (a / ((a + b) + d)) + (b / ((a + b) + c))
by XCMPLX_1:60;
a + (c + d) > c + d
by XREAL_1:29;
then A3:
d / (c + d) > d / ((a + c) + d)
by XREAL_1:76;
b + (c + d) > c + d
by XREAL_1:29;
then
c / (c + d) > c / ((b + c) + d)
by XREAL_1:76;
then
1 + (c / (c + d)) > ((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))
by A2, XREAL_1:8;
then
(1 + (c / (c + d))) + (d / (c + d)) > (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d))
by A3, XREAL_1:8;
then
1 + ((c / (c + d)) + (d / (c + d))) > (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d))
;
then
1 + ((c + d) / (c + d)) > (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d))
by XCMPLX_1:62;
then
1 + 1 > (((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d))
by XCMPLX_1:60;
hence
(((a / ((a + b) + d)) + (b / ((a + b) + c))) + (c / ((b + c) + d))) + (d / ((a + c) + d)) < 2
; verum