let w, x, y, z be ext-real number ; :: thesis: ( -infty < w & x < y & w < z implies x + w < y + z )
assume A1: -infty < w ; :: thesis: ( not x < y or not w < z or x + w < y + z )
assume that
A2: x < y and
A3: w < z ; :: 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, Th47;
z <= +infty by XXREAL_0:4;
then w in REAL by A1, A3, XXREAL_0:14;
then x + w < y + w by A2, Th47;
hence x + w < y + z by A7, XXREAL_0:2; :: thesis: verum

end;

end;