let Y be non empty Subset of ExtREAL; :: thesis: for r being R_eal st r in REAL holds
sup ({r} + Y) = (sup {r}) + (sup Y)
let r be R_eal; :: thesis: ( r in REAL implies sup ({r} + Y) = (sup {r}) + (sup Y) )
set X = {r};
assume A2: r in REAL ; :: thesis: sup ({r} + Y) = (sup {r}) + (sup Y)
set W = {r} + Y;
A3: - r <> -infty by A2, XXREAL_3:23;
A4: - r <> +infty by A2, XXREAL_3:23;

now

let z be set ; :: thesis: ( z in (- {r}) + ({r} + Y) implies z in Y )
assume z in (- {r}) + ({r} + Y) ; :: thesis: z in Y
then consider x, y being R_eal such that
A7: z = x + y and
A5: x in - {r} and
A6: y in {r} + Y ;
consider x1, y1 being R_eal such that
A10: y = x1 + y1 and
A8: x1 in {r} and
A9: y1 in Y by A6;
- x in - (- {r}) by A5, SUPINF_2:23;
then - x in {r} by SUPINF_2:22;
then - x = r by TARSKI:def 1;
then z = (- r) + (r + y1) by A7, A8, A10, TARSKI:def 1;
then z = ((- r) + r) + y1 by A2, A4, A3, XXREAL_3:30;
then z = 0. + y1 by XXREAL_3:7;
hence z in Y by A9, XXREAL_3:4; :: thesis: verum

end;

then A11: (- {r}) + ({r} + Y) c= Y by TARSKI:def 3;
A12: r in {r} by TARSKI:def 1;

now

let z be set ; :: thesis: ( z in Y implies z in (- {r}) + ({r} + Y) )
assume A13: z in Y ; :: thesis: z in (- {r}) + ({r} + Y)
then reconsider y = z as Element of ExtREAL ;
(r + y) - r = ((- r) + r) + y by A2, A4, A3, XXREAL_3:30;
then (r + y) - r = 0. + y by XXREAL_3:7;
then A14: y = (r + y) - r by XXREAL_3:4;
A15: - r in - {r} by A12;
r + y in {r} + Y by A12, A13;
hence z in (- {r}) + ({r} + Y) by A15, A14; :: thesis: verum

end;

then Y c= (- {r}) + ({r} + Y) by TARSKI:def 3;
then Y = (- {r}) + ({r} + Y) by A11, XBOOLE_0:def 10;
then sup Y <= (sup ({r} + Y)) + (sup (- {r})) by SUPINF_2:26;
then sup Y <= (sup ({r} + Y)) + (- (inf {r})) by SUPINF_2:33;
then sup Y <= (sup ({r} + Y)) - r by XXREAL_2:13;
then r + (sup Y) <= sup ({r} + Y) by A2, XXREAL_3:68;
then A16: (sup {r}) + (sup Y) <= sup ({r} + Y) by XXREAL_2:11;
sup ({r} + Y) <= (sup {r}) + (sup Y) by SUPINF_2:26;
hence sup ({r} + Y) = (sup {r}) + (sup Y) by A16, XXREAL_0:1; :: thesis: verum