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

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

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

then A4: ( x <> +infty & y <> +infty & z <> -infty ) by A1, A2, Th26;
-infty <= z by XXREAL_0:5;
then ( -infty < z & x + y = -infty ) by A3, A4, SUPINF_2:def 2, XXREAL_0:1;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by A1, A2, A3, Th26; :: thesis: verum

end;

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

-infty <= x by XXREAL_0:5;
then -infty < z - y by A2, XXREAL_0:2;
then A6: ( z <> -infty & y <> +infty ) by A1, Th26;
A7: z - y <= +infty by XXREAL_0:4;
then reconsider a = x as Real by A2, A5, XXREAL_0:14;

now

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

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

then ( z <> -infty & -infty <= z ) by A1, XXREAL_0:5;
then -infty < z by XXREAL_0:1;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by A2, A7, A8, SUPINF_2:def 2; :: thesis: verum

end;

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

then reconsider b = y as Real by A6, XXREAL_0:14;

now

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

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

x + y = a + b by SUPINF_2:1;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by A9, XXREAL_0:9; :: thesis: verum

end;

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

then reconsider c = z as Real by A6, XXREAL_0:14;
A10: ( x = a & z - y = c - b ) by SUPINF_2:5;
a + b < c by A2, A10, XREAL_1:22;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by SUPINF_2:1; :: thesis: verum

end;

end;

end;

hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) ; :: thesis: verum

end;

end;

end;

hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) ; :: thesis: verum

end;

end;