let x, y, z, w be ext-real number ; :: thesis: ( x <= y & z <= w implies x + z <= y + w )
assume A1: ( x <= y & z <= w ) ; :: thesis: x + z <= y + w

per cases ( ( x = +infty & z = -infty ) or ( x = -infty & z = +infty ) or ( y = +infty & w = -infty ) or ( y = -infty & w = +infty ) or ( not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) & not ( y = +infty & w = -infty ) & not ( y = -infty & w = +infty ) ) ) ;

suppose S: ( x = +infty & z = -infty ) ; :: thesis: x + z <= y + w

then A: y = +infty by A1, XXREAL_0:4;
( w <> -infty implies +infty + w = +infty ) by Def3;
hence x + z <= y + w by A, S; :: thesis: verum

end;

suppose S: ( x = -infty & z = +infty ) ; :: thesis: x + z <= y + w

then A: w = +infty by A1, XXREAL_0:4;
( y <> -infty implies +infty + y = +infty ) by Def3;
hence x + z <= y + w by A, S; :: thesis: verum

end;

suppose S: ( y = +infty & w = -infty ) ; :: thesis: x + z <= y + w

then A: z = -infty by A1, XXREAL_0:6;
( x <> +infty implies -infty + x = -infty ) by Def3;
hence x + z <= y + w by A, S; :: thesis: verum

end;

suppose S: ( y = -infty & w = +infty ) ; :: thesis: x + z <= y + w

then A: x = -infty by A1, XXREAL_0:6;
( z <> +infty implies -infty + z = -infty ) by Def3;
hence x + z <= y + w by A, S; :: thesis: verum

end;

suppose S: ( not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) & not ( y = +infty & w = -infty ) & not ( y = -infty & w = +infty ) ) ; :: thesis: x + z <= y + w

reconsider a = x + z, b = y + w as Element of ExtREAL by XXREAL_0:def 1;
A2: ( ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a in REAL & b = -infty ) or ( a = +infty & b in REAL ) or ( a = +infty & b = +infty ) or ( a = +infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a = -infty & b = -infty ) ) by XXREAL_0:14;
A3: ( a in REAL & b in REAL implies a <= b )

proof

assume ( a in REAL & b in REAL ) ; :: thesis: a <= b
then ( x in REAL & y in REAL & z in REAL & w in REAL ) by Th34, S;
then consider Ox, Oy, Os, Ot being real number such that
A4: ( Ox = x & Oy = y & Os = z & Ot = w & Ox <= Oy & Os <= Ot ) by A1;
A5: Ox + Os <= Os + Oy by A4, XREAL_1:8;
Os + Oy <= Ot + Oy by A4, XREAL_1:8;
hence a <= b by A5, A4, XXREAL_0:2; :: thesis: verum

end;

A7: ( a in REAL & b = -infty implies a <= b )

proof

assume ( a in REAL & b = -infty ) ; :: thesis: a <= b
then ( y = -infty or w = -infty ) by LTh9;
then ( x = -infty or z = -infty ) by A1, XXREAL_0:6;
then a = -infty by Def3, S;
hence a <= b by XXREAL_0:5; :: thesis: verum

end;

A8: ( a = +infty & b in REAL implies a <= b )

proof

assume ( a = +infty & b in REAL ) ; :: thesis: a <= b
then ( x = +infty or z = +infty ) by LTh8;
then ( y = +infty or w = +infty ) by A1, XXREAL_0:4;
then b = +infty by Def3, S;
hence a <= b by XXREAL_0:4; :: thesis: verum

end;

( not a = +infty or not b = -infty )

proof

assume A9: ( a = +infty & b = -infty ) ; :: thesis: contradiction
( x = +infty or z = +infty ) by A9, LTh8;
hence contradiction by A1, A9, S, XXREAL_0:4, LTh9; :: thesis: verum

end;

hence x + z <= y + w by A2, A3, A7, A8, XXREAL_0:4, XXREAL_0:5; :: thesis: verum

end;

end;