let a1, a2, a3, a4, a5, a6, b1, b2, b3, b4, b5, b6 be Real; ( 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 that
A1:
a1 >= b1
and
A2:
a2 >= b2
and
A3:
a3 >= b3
and
A4:
a4 >= b4
and
A5:
a5 >= b5
and
A6:
a6 >= b6
; ((((a1 + a2) + a3) + a4) + a5) + a6 >= ((((b1 + b2) + b3) + b4) + b5) + b6
A7:
a1 + a2 >= b1 + b2
by A1, A2, XREAL_1:7;
A8:
a3 + a4 >= b3 + b4
by A3, A4, XREAL_1:7;
A9:
a5 + a6 >= b5 + b6
by A5, A6, XREAL_1:7;
(a1 + a2) + (a3 + a4) >= (b1 + b2) + (b3 + b4)
by A7, A8, XREAL_1:7;
then
((a1 + a2) + (a3 + a4)) + (a5 + a6) >= ((b1 + b2) + (b3 + b4)) + (b5 + b6)
by A9, XREAL_1:7;
hence
((((a1 + a2) + a3) + a4) + a5) + a6 >= ((((b1 + b2) + b3) + b4) + b5) + b6
; verum