let x, y, z be ExtReal; :: 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, Def2;
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, Th13;
hence x <= z - y by XXREAL_0:4; :: thesis: verum

end;

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

then A5: x + y < +infty by A2, XXREAL_0:2, XXREAL_0:4;
then A6: x <> +infty by A1, Def2;
A7: y <> +infty by A1, A5, Def2;

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 A6, XXREAL_0:14;
then reconsider a = x as Real ;

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

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

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

end;

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

then y in REAL by A7, XXREAL_0:14;
then reconsider b = y as Real ;
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 ;
x + y = a + b ;
then a <= c - b by A2, XREAL_1:19;
hence x <= z - y ; :: thesis: verum

end;

end;

end;

end;

end;

end;