let x, y, z be R_eal; :: thesis: ( ( not x = +infty or not y = -infty ) & ( not x = -infty or not y = +infty ) & ( not y = +infty or not z = +infty ) & x <= z - y implies ( y <> +infty & x + y <= z ) )
assume that
A1: ( not x = +infty or not y = -infty ) and
A2: ( not x = -infty or not y = +infty ) and
A3: ( not y = +infty or not z = +infty ) and
A4: x <= z - y ; :: thesis: ( y <> +infty & x + y <= z )
thus A5: y <> +infty :: thesis: x + y <= z

proof

assume A6: y = +infty ; :: thesis: contradiction
then z - y = -infty by A3, SUPINF_2:6;
hence contradiction by A2, A4, A6, XXREAL_0:6; :: thesis: verum

end;

per cases ( y = -infty or ( y <> +infty & y <> -infty ) ) by A5;

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

then x + y = -infty by A1, SUPINF_2:def 2;
hence x + y <= z by XXREAL_0:5; :: thesis: verum

end;

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

then A8: y is Real by XXREAL_0:14;
( - +infty = -infty & - -infty = +infty ) by SUPINF_2:4;
then ( - y <> -infty & - y <> +infty ) by A7;
then (z - y) + y = z + ((- y) + y) by A7, EXTREAL1:8
.= z + 0. by EXTREAL1:9
.= z by SUPINF_2:18 ;
hence x + y <= z by A4, A8, MEASURE6:11; :: thesis: verum

end;

end;