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

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

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

then ( x <> +infty & y <> +infty & z <> -infty ) by A1, A2, Def3;
then ( x < +infty & z - y = +infty ) by A3, XXREAL_0:4, Th16;
hence ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) by A1, A2, A3, Def3; :: thesis: verum

end;

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

x + y < +infty by A2, XXREAL_0:2, XXREAL_0:4;
then A5: ( x <> +infty & y <> +infty ) by A1, Def3;
A6: -infty <= x + y by XXREAL_0:5;
then z in REAL by A2, A4, XXREAL_0:14;
then reconsider c = z as real number ;

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

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

then x < +infty by A1, XXREAL_0:4;
hence ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) by A2, A6, A7, Th29; :: thesis: verum

end;

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

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

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

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

X: z - y = c - b ;
thus x <> +infty by A8; :: thesis: ( y <> +infty & z <> -infty & x < z - y )
thus y <> +infty by X; :: thesis: ( z <> -infty & x < z - y )
thus z <> -infty by X; :: thesis: x < z - y
c - b in REAL by XREAL_0:def 1;
hence x < z - y by A8, XXREAL_0:12; :: thesis: verum

end;

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

then x in REAL by A5, XXREAL_0:14;
then reconsider a = x as real number ;
A9: ( x + y = a + b & z = c ) ;
a < c - b by A2, A9, XREAL_1:22;
hence ( x <> +infty & y <> +infty & z <> -infty & x < z - y ) ; :: thesis: verum

end;

end;

end;

end;

end;

end;