let x, y, z be R_eal; :: 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, Th25;
then ( x < +infty & z + y = +infty ) by A3, SUPINF_2:def 2, XXREAL_0:4;
hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) by A1, A2, A3, Th25; :: 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, Th25;
A6: -infty <= x - y by XXREAL_0:5;
then reconsider c = z as Real by A2, A4, XXREAL_0:14;
now
per cases ( y = +infty or y <> +infty ) ;
suppose y <> +infty ; :: thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y )
then reconsider b = y as Real by A5, XXREAL_0:14;
now
per cases ( x = -infty or x <> -infty ) ;
suppose A8: x = -infty ; :: thesis: ( x <> +infty & y <> -infty & z <> -infty & x < z + y )
z + y = c + b by SUPINF_2:1;
hence ( x <> +infty & y <> -infty & z <> -infty & 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 reconsider a = x as Real by A5, XXREAL_0:14;
A9: ( x - y = a - b & z = c ) by SUPINF_2:5;
a < c + b by A2, A9, XREAL_1:21;
hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) by SUPINF_2:1; :: thesis: verum
end;
end;
end;
hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) ; :: thesis: verum
end;
end;
end;
hence ( x <> +infty & y <> -infty & z <> -infty & x < z + y ) ; :: thesis: verum
end;
end;