let a, b, c, d be positive Real; :: thesis: (((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 ;
a / (a + b) > a / ((a + b) + d) by ;
then (a / (a + b)) + (b / (a + b)) > (a / ((a + b) + d)) + (b / ((a + b) + c)) by ;
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 ;
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 ;
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 ; :: thesis: verum