let x, y, z, w be ExtReal; :: thesis: ( x <= y & z <= w implies x + z <= y + w )
assume that
A1: x <= y and
A2: z <= w ; :: thesis: x + z <= y + w
per cases ( ( x = +infty & z = -infty ) or ( x = -infty & z = +infty ) or ( y = +infty & w = -infty ) or ( y = -infty & w = +infty ) or ( not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) & not ( y = +infty & w = -infty ) & not ( y = -infty & w = +infty ) ) ) ;
suppose A3: ( x = +infty & z = -infty ) ; :: thesis: x + z <= y + w
A4: ( w <> -infty implies +infty + w = +infty ) by Def2;
y = +infty by A1, A3, XXREAL_0:4;
hence x + z <= y + w by A3, A4; :: thesis: verum
end;
suppose A5: ( x = -infty & z = +infty ) ; :: thesis: x + z <= y + w
A6: ( y <> -infty implies +infty + y = +infty ) by Def2;
w = +infty by A2, A5, XXREAL_0:4;
hence x + z <= y + w by A5, A6; :: thesis: verum
end;
suppose A7: ( y = +infty & w = -infty ) ; :: thesis: x + z <= y + w
A8: ( x <> +infty implies -infty + x = -infty ) by Def2;
z = -infty by A2, A7, XXREAL_0:6;
hence x + z <= y + w by A7, A8; :: thesis: verum
end;
suppose A9: ( y = -infty & w = +infty ) ; :: thesis: x + z <= y + w
A10: ( z <> +infty implies -infty + z = -infty ) by Def2;
x = -infty by A1, A9, XXREAL_0:6;
hence x + z <= y + w by A9, A10; :: thesis: verum
end;
suppose A11: ( not ( x = +infty & z = -infty ) & not ( x = -infty & z = +infty ) & not ( y = +infty & w = -infty ) & not ( y = -infty & w = +infty ) ) ; :: thesis: x + z <= y + w
reconsider a = x + z, b = y + w as Element of ExtREAL by XXREAL_0:def 1;
A12: ( not a = +infty or not b = -infty ) A15: ( a in REAL & b in REAL implies a <= b )
proof
assume A16: ( a in REAL & b in REAL ) ; :: thesis: a <= b
then A17: ( z in REAL & w in REAL ) by A11, Th20;
( x in REAL & y in REAL ) by A11, A16, Th20;
then consider Ox, Oy, Os, Ot being Real such that
A18: ( Ox = x & Oy = y & Os = z & Ot = w ) and
A19: ( Ox <= Oy & Os <= Ot ) by A1, A2, A17;
( Ox + Os <= Os + Oy & Os + Oy <= Ot + Oy ) by A19, XREAL_1:6;
hence a <= b by A18, XXREAL_0:2; :: thesis: verum
end;
A20: ( a = +infty & b in REAL implies a <= b ) A22: ( a in REAL & b = -infty implies a <= b ) ( ( a in REAL & b in REAL ) or ( a in REAL & b = +infty ) or ( a in REAL & b = -infty ) or ( a = +infty & b in REAL ) or ( a = +infty & b = +infty ) or ( a = +infty & b = -infty ) or ( a = -infty & b in REAL ) or ( a = -infty & b = +infty ) or ( a = -infty & b = -infty ) ) by XXREAL_0:14;
hence x + z <= y + w by A15, A22, A20, A12, XXREAL_0:4, XXREAL_0:5; :: thesis: verum
end;
end;