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

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

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

per cases ( x = -infty or y = +infty ) by A3, A4, Th19, XXREAL_0:6;

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

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

end;

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

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

end;

end;

end;

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

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

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

hence x <= z + y by A2, A5; :: thesis: verum

end;

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

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

end;

end;

end;

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

per cases ( x - y in REAL or x - y = -infty ) by A3, A6, XXREAL_0:13;

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

per cases ( y = +infty or x = -infty or ( x in REAL & y in REAL ) ) by A7, Th21;

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

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

end;

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

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

end;

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

then reconsider a = x, b = y, c = z as Element of REAL by A6;
a - b <= c by A3;
then a <= b + c by XREAL_1:20;
hence x <= z + y ; :: thesis: verum

end;

end;

end;

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

per cases ( x = -infty or y = +infty ) by A8, Th19;

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

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

end;

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

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

end;

end;

end;

end;

end;

end;