let x, y, z be ExtReal; :: 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 )
A4: -infty <= z by XXREAL_0:5;
z <> -infty by A1, A2, A3, Def2;
then A5: -infty < z by A4, XXREAL_0:1;
y <> -infty by A1, A2, A3, Def2;
hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) by A3, A5, Th14; :: thesis: verum
end;
suppose A6: x <> -infty ; :: thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z )
A7: z + y <= +infty by XXREAL_0:4;
then x in REAL by A2, A6, XXREAL_0:14;
then reconsider a = x as Real ;
A8: -infty <= x by XXREAL_0:5;
then A9: z <> -infty by A1, A2, Def2;
A10: y <> -infty by A1, A2, A8, Def2;
per cases ( y = +infty or y <> +infty ) ;
suppose y <> +infty ; :: thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z )
then y in REAL by A10, XXREAL_0:14;
then reconsider b = y as Real ;
per cases ( z = +infty or z <> +infty ) ;
suppose z <> +infty ; :: thesis: ( x <> +infty & y <> -infty & z <> -infty & x - y < z )
then z in REAL by A9, XXREAL_0:14;
then reconsider c = z as Real ;
z + y = c + b ;
then a - b < c by A2, XREAL_1:19;
hence ( x <> +infty & y <> -infty & z <> -infty & x - y < z ) ; :: thesis: verum
end;
end;
end;
end;
end;
end;