let x, y, z, w be ExtReal; :: thesis: ( x <= y & z <= w implies x + z <= y + w )
assume that
A1: x <= y and
A2: 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 A3: ( x = +infty & z = -infty ) ; :: thesis: x + z <= y + w

A4: ( w <> -infty implies +infty + w = +infty ) by Def2;
y = +infty by A1, A3, XXREAL_0:4;
hence x + z <= y + w by A3, A4; :: thesis: verum

end;

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

A6: ( y <> -infty implies +infty + y = +infty ) by Def2;
w = +infty by A2, A5, XXREAL_0:4;
hence x + z <= y + w by A5, A6; :: thesis: verum

end;

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

A8: ( x <> +infty implies -infty + x = -infty ) by Def2;
z = -infty by A2, A7, XXREAL_0:6;
hence x + z <= y + w by A7, A8; :: thesis: verum

end;

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

A10: ( z <> +infty implies -infty + z = -infty ) by Def2;
x = -infty by A1, A9, XXREAL_0:6;
hence x + z <= y + w by A9, A10; :: thesis: verum

end;

suppose A11: ( 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;
A12: ( not a = +infty or not b = -infty )

proof

assume that
A13: a = +infty and
A14: b = -infty ; :: thesis: contradiction
( x = +infty or z = +infty ) by A13, Lm8;
hence contradiction by A1, A2, A11, A14, Lm9, XXREAL_0:4; :: thesis: verum

end;

A15: ( a in REAL & b in REAL implies a <= b )

proof

assume A16: ( a in REAL & b in REAL ) ; :: thesis: a <= b
then A17: ( z in REAL & w in REAL ) by A11, Th20;
( x in REAL & y in REAL ) by A11, A16, Th20;
then consider Ox, Oy, Os, Ot being Real such that
A18: ( Ox = x & Oy = y & Os = z & Ot = w ) and
A19: ( Ox <= Oy & Os <= Ot ) by A1, A2, A17;
( Ox + Os <= Os + Oy & Os + Oy <= Ot + Oy ) by A19, XREAL_1:6;
hence a <= b by A18, XXREAL_0:2; :: thesis: verum

end;

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

proof

assume that
A21: a = +infty and
b in REAL ; :: thesis: a <= b
( x = +infty or z = +infty ) by A21, Lm8;
then ( y = +infty or w = +infty ) by A1, A2, XXREAL_0:4;
then b = +infty by A11, Def2;
hence a <= b by XXREAL_0:4; :: thesis: verum

end;

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

proof

assume that
a in REAL and
A23: b = -infty ; :: thesis: a <= b
( y = -infty or w = -infty ) by A23, Lm9;
then ( x = -infty or z = -infty ) by A1, A2, XXREAL_0:6;
then a = -infty by A11, Def2;
hence a <= b by XXREAL_0:5; :: thesis: verum

end;

( ( 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;
hence x + z <= y + w by A15, A22, A20, A12, XXREAL_0:4, XXREAL_0:5; :: thesis: verum

end;

end;