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

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

end;

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

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

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

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

end;

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

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

end;

end;

end;

end;