let a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 be real number ; :: thesis: ( a1 >= b1 & a2 >= b2 & a3 >= b3 & a4 >= b4 & a5 >= b5 & a6 >= b6 implies ((((a1 + a2) + a3) + a4) + a5) + a6 >= ((((b1 + b2) + b3) + b4) + b5) + b6 )
assume ( a1 >= b1 & a2 >= b2 & a3 >= b3 & a4 >= b4 & a5 >= b5 & a6 >= b6 ) ; :: thesis: ((((a1 + a2) + a3) + a4) + a5) + a6 >= ((((b1 + b2) + b3) + b4) + b5) + b6
then A1: ( a1 + a2 >= b1 + b2 & a3 + a4 >= b3 + b4 & a5 + a6 >= b5 + b6 ) by XREAL_1:9;
then (a1 + a2) + (a3 + a4) >= (b1 + b2) + (b3 + b4) by XREAL_1:9;
then ((a1 + a2) + (a3 + a4)) + (a5 + a6) >= ((b1 + b2) + (b3 + b4)) + (b5 + b6) by A1, XREAL_1:9;
hence ((((a1 + a2) + a3) + a4) + a5) + a6 >= ((((b1 + b2) + b3) + b4) + b5) + b6 ; :: thesis: verum