let z, y, x be ext-real number ; :: thesis: ( ( z = -infty & y = +infty implies x <= 0 ) & ( z = +infty & y = -infty implies x <= 0 ) & x - y <= z implies x <= z + y )
assume that
Z1: ( z = -infty & y = +infty implies x <= 0 ) and
Z2: ( z = +infty & y = -infty implies x <= 0 ) and
Z3: x - y <= z ; :: thesis: x <= z + y

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

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

per cases ( x = -infty or y = +infty ) by S, Th33, Z3, 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 Z1, S; :: thesis: verum

end;

end;

end;

suppose S: 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 Z2, S; :: thesis: verum

end;

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

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

end;

end;

end;

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

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

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

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

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

then z + y = +infty by S, Def3;
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 that S1: x in REAL and
S2: y in REAL ; :: thesis: x <= z + y

reconsider a = x, b = y, c = z as Element of REAL by S, S1, S2;
a - b <= c by Z3;
then a <= b + c by XREAL_1:22;
hence x <= z + y ; :: thesis: verum

end;

end;

end;

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

per cases ( x = -infty or y = +infty ) by SS, Th33;

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 S, Def3;
hence x <= z + y by XXREAL_0:3; :: thesis: verum

end;

end;

end;

end;

end;

end;