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, Def3;
-infty <= z by XXREAL_0:5;
then ( -infty < z & x - y = -infty ) by A3, A4, XXREAL_0:1, Th29;
hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) by A1, A2, A3, Def3; :: 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, Def3, 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, Th16; :: 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 ;
A10: ( x = a & z + y = c + b ) ;
a - b < c by A2, A10, XREAL_1:21;
hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) ; :: thesis: verum

end;

end;

end;

end;

end;

end;