let x, y, s, t be R_eal; :: thesis: ( x <= y & s <= t implies x + s <= y + t )
assume A1: ( x <= y & s <= t ) ; :: thesis: x + s <= y + t

per cases ( ( x = +infty & s = -infty ) or ( x = -infty & s = +infty ) or ( y = +infty & t = -infty ) or ( y = -infty & t = +infty ) or ( not ( x = +infty & s = -infty ) & not ( x = -infty & s = +infty ) & not ( y = +infty & t = -infty ) & not ( y = -infty & t = +infty ) ) ) ;

suppose S: ( x = +infty & s = -infty ) ; :: thesis: x + s <= y + t

then A: y = +infty by A1, XXREAL_0:4;
( t <> -infty implies +infty + t = +infty ) by Def2;
hence x + s <= y + t by A, S, XXREAL_0:3; :: thesis: verum

end;

suppose S: ( x = -infty & s = +infty ) ; :: thesis: x + s <= y + t

then A: t = +infty by A1, XXREAL_0:4;
( y <> -infty implies +infty + y = +infty ) by Def2;
hence x + s <= y + t by A, S, XXREAL_0:3; :: thesis: verum

end;

suppose S: ( y = +infty & t = -infty ) ; :: thesis: x + s <= y + t

then A: s = -infty by A1, XXREAL_0:6;
( x <> +infty implies -infty + x = -infty ) by Def2;
hence x + s <= y + t by A, S, XXREAL_0:5; :: thesis: verum

end;

suppose S: ( y = -infty & t = +infty ) ; :: thesis: x + s <= y + t

then A: x = -infty by A1, XXREAL_0:6;
( s <> +infty implies -infty + s = -infty ) by Def2;
hence x + s <= y + t by A, S, XXREAL_0:5; :: thesis: verum

end;

suppose S: ( not ( x = +infty & s = -infty ) & not ( x = -infty & s = +infty ) & not ( y = +infty & t = -infty ) & not ( y = -infty & t = +infty ) ) ; :: thesis: x + s <= y + t

reconsider a = x + s, b = y + t as R_eal ;
( ( a in REAL or a in {-infty ,+infty } ) & ( b in REAL or b in {-infty ,+infty } ) ) by XBOOLE_0:def 3;
then A2: ( ( 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 TARSKI:def 2;
A3: ( a in REAL & b in REAL implies a <= b )

proof

assume ( a in REAL & b in REAL ) ; :: thesis: a <= b
then ( x is Real & y is Real & s is Real & t is Real ) by Th12, S;
then consider Ox, Oy, Os, Ot being Real such that
A4: ( Ox = x & Oy = y & Os = s & Ot = t & Ox <= Oy & Os <= Ot ) by A1;
A5: Ox + Os <= Os + Oy by A4, XREAL_1:8;
A6: Os + Oy <= Ot + Oy by A4, XREAL_1:8;
( x + s = Ox + Os & y + t = Oy + Ot ) by A4, Th1;
hence a <= b by A5, A6, XXREAL_0:2; :: thesis: verum

end;

A7: ( a in REAL & b = -infty implies a <= b )

proof

assume ( a in REAL & b = -infty ) ; :: thesis: a <= b
then ( y = -infty or t = -infty ) by Th9;
then ( x = -infty or s = -infty ) by A1, XXREAL_0:6;
then a = -infty by Def2, S;
hence a <= b by XXREAL_0:5; :: thesis: verum

end;

A8: ( a = +infty & b in REAL implies a <= b )

proof

assume ( a = +infty & b in REAL ) ; :: thesis: a <= b
then ( x = +infty or s = +infty ) by Th8;
then ( y = +infty or t = +infty ) by A1, XXREAL_0:4;
then b = +infty by Def2, S;
hence a <= b by XXREAL_0:4; :: thesis: verum

end;

( not a = +infty or not b = -infty )

proof

assume A9: ( a = +infty & b = -infty ) ; :: thesis: contradiction
then A10: ( y = -infty or t = -infty ) by Th9;
( x = +infty or s = +infty ) by A9, Th8;
hence contradiction by A1, A10, S, XXREAL_0:4; :: thesis: verum

end;

hence x + s <= y + t by A2, A3, A7, A8, XXREAL_0:4, XXREAL_0:5; :: thesis: verum

end;

end;