let x, y, z be ext-real number ; :: thesis: ( ( x = +infty & y = +infty implies 0 <= z ) & ( x = -infty & y = -infty implies 0 <= z ) & x <= z + y implies x - y <= z )
assume that
Z1: ( x = +infty & y = +infty implies 0 <= z ) and
Z2: ( x = -infty & y = -infty implies 0 <= z ) and
Z3: x <= z + y ; :: thesis: x - y <= z
per cases ( x = +infty or x = -infty or x in REAL ) by XXREAL_0:14;
suppose S: x = +infty ; :: thesis: x - y <= z
end;
suppose S: x = -infty ; :: thesis: x - y <= z
end;
suppose S: x in REAL ; :: thesis: x - y <= z
per cases ( z + y in REAL or z + y = +infty ) by Z3, S, XXREAL_0:10;
suppose SS: z + y in REAL ; :: thesis: x - y <= z
per cases ( y = +infty or z = +infty or ( z in REAL & y in REAL ) ) by SS, Th34;
suppose that S1: z in REAL and
S2: y in REAL ; :: thesis: x - y <= z
reconsider a = x, b = y, c = z as Element of REAL by S, S1, S2;
a <= b + c by Z3;
then a - b <= c by XREAL_1:22;
hence x - y <= z ; :: thesis: verum
end;
end;
end;
end;
end;
end;