let x, y, z, w be ExtReal; :: thesis: ( x < y & w < z implies x + w < y + z )
assume that
A1: x < y and
A2: w < z ; :: thesis: x + w < y + z
-infty <= w by XXREAL_0:5;

per cases then ( w = -infty or -infty < w ) by XXREAL_0:1;

suppose A3: w = -infty ; :: thesis: x + w < y + z

A4: ( y <> -infty & z <> -infty ) by A1, A2, XXREAL_0:5;
x <> +infty by A1, XXREAL_0:3;
then x + w = -infty by A3, Def2;
hence x + w < y + z by A4, Lm9, XXREAL_0:6; :: thesis: verum

end;

suppose A5: -infty < w ; :: thesis: x + w < y + z

per cases ( y = +infty or y <> +infty ) ;

suppose A6: y = +infty ; :: thesis: x + w < y + z

A7: z <= +infty by XXREAL_0:4;
y + z = +infty by A5, A2, A6, Def2;
hence x + w < y + z by A1, A2, A6, A7, Lm8, XXREAL_0:4; :: thesis: verum

end;

suppose A8: y <> +infty ; :: thesis: x + w < y + z

-infty <= x by XXREAL_0:5;
then y in REAL by A1, A8, XXREAL_0:14;
then A9: y + w < y + z by A2, Th43;
z <= +infty by XXREAL_0:4;
then w in REAL by A5, A2, XXREAL_0:14;
then x + w < y + w by A1, Th43;
hence x + w < y + z by A9, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;