let x, y, z be ExtReal; :: 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 by A1, A2, Th13;
then A4: x < +infty by XXREAL_0:4;
y <> -infty by A1, A2, A3, Th14;
hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) by A3, A4, Def2; :: thesis: verum

end;

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

A6: -infty <= x - y by XXREAL_0:5;
then z in REAL by A2, A5, XXREAL_0:14;
then reconsider c = z as Real ;
A7: x - y < +infty by A2, XXREAL_0:2, XXREAL_0:4;
then A8: x <> +infty by A1, Th13;
A9: y <> -infty by A1, A7, Th14;

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

suppose A10: 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, A10, Def2; :: thesis: verum

end;

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

then y in REAL by A9, XXREAL_0:14;
then reconsider b = y as Real ;

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

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

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

end;

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

then x in REAL by A8, XXREAL_0:14;
then reconsider a = x as Real ;
x - y = a - b ;
then a < c + b by A2, XREAL_1:19;
hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) ; :: thesis: verum

end;

end;

end;

end;

end;

end;