let x, y, z be ExtReal; :: thesis: ( x <= y implies x + z <= y + z )
assume A1: x <= y ; :: thesis: x + z <= y + z

per cases ( ( x in REAL & y in REAL ) or ( x in REAL & y = +infty ) or ( x = -infty & y in REAL ) or ( x = -infty & y = +infty ) or x = +infty or y = -infty ) by XXREAL_0:14;

suppose A2: ( x in REAL & y in REAL ) ; :: thesis: x + z <= y + z

per cases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;

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

-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by A2, A3, Def2; :: thesis: verum

end;

suppose z in REAL ; :: thesis: x + z <= y + z

then reconsider x = x, y = y, z = z as Real by A2;
x + z <= y + z by A1, XREAL_1:6;
hence x + z <= y + z ; :: thesis: verum

end;

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

x + z <= +infty by XXREAL_0:3;
hence x + z <= y + z by A2, A4, Def2; :: thesis: verum

end;

end;

end;

suppose A5: ( x in REAL & y = +infty ) ; :: thesis: x + z <= y + z

per cases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;

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

-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by A5, A6, Def2; :: thesis: verum

end;

suppose A7: z in REAL ; :: thesis: x + z <= y + z

x + z <= +infty by XXREAL_0:3;
hence x + z <= y + z by A5, A7, Def2; :: thesis: verum

end;

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

hence x + z <= y + z by A5, Lm1, XXREAL_0:3; :: thesis: verum

end;

end;

end;

suppose A8: ( x = -infty & y in REAL ) ; :: thesis: x + z <= y + z

per cases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;

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

hence x + z <= y + z by A8, Lm2, XXREAL_0:5; :: thesis: verum

end;

suppose A9: z in REAL ; :: thesis: x + z <= y + z

-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by A8, A9, Def2; :: thesis: verum

end;

suppose A10: z = +infty ; :: thesis: x + z <= y + z

x + z <= +infty by XXREAL_0:3;
hence x + z <= y + z by A8, A10, Def2; :: thesis: verum

end;

end;

end;

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

per cases ( z = -infty or z in REAL or z = +infty ) by XXREAL_0:14;

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

hence x + z <= y + z by A11, Lm2; :: thesis: verum

end;

suppose A12: z in REAL ; :: thesis: x + z <= y + z

-infty <= y + z by XXREAL_0:5;
hence x + z <= y + z by A11, A12, Def2; :: thesis: verum

end;

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

hence x + z <= y + z by A11, Lm1; :: thesis: verum

end;

end;

end;

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

hence x + z <= y + z by A1, XXREAL_0:4; :: thesis: verum

end;

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

hence x + z <= y + z by A1, XXREAL_0:6; :: thesis: verum

end;

end;