let x, y, z be ExtReal; :: thesis: ( ( x = +infty & y = +infty implies 0 <= z ) & ( x = -infty & y = -infty implies 0 <= z ) & x <= z + y implies x - y <= z )
assume that
A1: ( x = +infty & y = +infty implies 0 <= z ) and
A2: ( x = -infty & y = -infty implies 0 <= z ) and
A3: x <= z + y ; :: thesis: x - y <= z
per cases ( x = +infty or x = -infty or x in REAL ) by XXREAL_0:14;
suppose A4: x = +infty ; :: thesis: x - y <= z
end;
suppose A5: x = -infty ; :: thesis: x - y <= z
end;
suppose A6: x in REAL ; :: thesis: x - y <= z
per cases ( z + y in REAL or z + y = +infty ) by A3, A6, XXREAL_0:10;
suppose A7: z + y in REAL ; :: thesis: x - y <= z
per cases ( y = +infty or z = +infty or ( z in REAL & y in REAL ) ) by A7, Th20;
suppose ( z in REAL & y in REAL ) ; :: thesis: x - y <= z
then reconsider a = x, b = y, c = z as Element of REAL by A6;
a <= b + c by A3;
then a - b <= c by XREAL_1:20;
hence x - y <= z ; :: thesis: verum
end;
end;
end;
end;
end;
end;