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