let x, y, z be ext-real number ; :: thesis: ( ( x = +infty & y = -infty ) or ( x = -infty & y = +infty ) or ( y = +infty & z = +infty ) or ( y = -infty & z = -infty ) or not x + y <= z or ( y <> +infty & x <= z - y ) )
assume that
A1: ( not ( x = +infty & y = -infty ) & not ( x = -infty & y = +infty ) & not ( y = +infty & z = +infty ) & not ( y = -infty & z = -infty ) ) and
A2: x + y <= z ; :: thesis: ( y <> +infty & x <= z - y )
thus y <> +infty :: thesis: x <= z - y

proof

assume A3: y = +infty ; :: thesis: contradiction
then x + y = +infty by A1, Def3;
hence contradiction by A1, A2, A3, XXREAL_0:4; :: thesis: verum

end;

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

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

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

end;

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

then x + y < +infty by A2, XXREAL_0:2, XXREAL_0:4;
then A5: ( x <> +infty & y <> +infty ) by A1, Def3;

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

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

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

end;

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

then x in REAL by A5, XXREAL_0:14;
then reconsider a = x as real number ;

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

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

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

end;

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

then y in REAL by A5, XXREAL_0:14;
then reconsider b = y as real number ;
A6: x + y = a + b ;
a + b in REAL by XREAL_0:def 1;
then z <> -infty by A2, XXREAL_0:12;
then z in REAL by A4, XXREAL_0:14;
then reconsider c = z as real number ;
z = c ;
then consider p, q being real number such that
A7: ( p = x + y & q = z & p <= q ) by A2, A6;
a <= c - b by A6, A7, XREAL_1:21;
hence x <= z - y ; :: thesis: verum

end;

end;

end;

end;

end;

end;