let z, y, x be ext-real number ; :: 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, Th16, Th29;
-infty <= z by XXREAL_0:5;
then ( -infty < z & x + y = -infty ) by A3, A4, XXREAL_0:1, Def3;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) by A3; :: thesis: verum

end;

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

-infty <= x by XXREAL_0:5;
then A6: ( z <> -infty & y <> +infty ) by A1, Th16, Th29, A2;
A7: z - y <= +infty by XXREAL_0:4;
then x in REAL by A2, A5, XXREAL_0:14;
then reconsider a = x as real number ;

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, Def3; :: thesis: verum

end;

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

then y in REAL by A6, XXREAL_0:14;
then reconsider b = y as real number ;

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

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

a + b in REAL by XREAL_0:def 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 z in REAL by A6, XXREAL_0:14;
then reconsider c = z as real number ;
( x = a & z - y = c - b ) ;
then a + b < c by A2, XREAL_1:22;
hence ( x <> +infty & y <> +infty & z <> -infty & x + y < z ) ; :: thesis: verum

end;

end;

end;

end;

end;

end;