let X, Y be non empty Subset of ExtREAL ; :: thesis: for r being R_eal st X = {r} & r in REAL holds
sup (X + Y) = (sup X) + (sup Y)
let r be R_eal; :: thesis: ( X = {r} & r in REAL implies sup (X + Y) = (sup X) + (sup Y) )
assume that
A1: X = {r} and
A2: r in REAL ; :: thesis: sup (X + Y) = (sup X) + (sup Y)
A5: sup (X + Y) <= (sup X) + (sup Y) by SUPINF_2:26;
set W = X + Y;
A8: ( - r <> +infty & - r <> -infty ) by A2, XXREAL_3:23;
A61: r in X by A1, TARSKI:def 1;

now

let z be set ; :: thesis: ( z in Y implies z in (- X) + (X + Y) )
assume A60: z in Y ; :: thesis: z in (- X) + (X + Y)
then reconsider y = z as Element of ExtREAL ;
A62: r + y in X + Y by A61, A60, SUPINF_2:def 5;
A63: - r in - X by A61, SUPINF_2:def 6;
(r + y) - r = ((- r) + r) + y by A2, A8, XXREAL_3:30;
then (r + y) - r = 0. + y by XXREAL_3:7;
then y = (r + y) - r by XXREAL_3:4;
hence z in (- X) + (X + Y) by A62, A63, SUPINF_2:def 5; :: thesis: verum

end;

then A64: Y c= (- X) + (X + Y) by TARSKI:def 3;

now

let z be set ; :: thesis: ( z in (- X) + (X + Y) implies z in Y )
assume z in (- X) + (X + Y) ; :: thesis: z in Y
then consider x, y being R_eal such that
A65: ( x in - X & y in X + Y & z = x + y ) by SUPINF_2:def 5;
- x in - (- X) by A65, SUPINF_2:23;
then - x in X by SUPINF_2:22;
then A66: - x = r by A1, TARSKI:def 1;
consider x1, y1 being R_eal such that
A67: ( x1 in X & y1 in Y & y = x1 + y1 ) by A65, SUPINF_2:def 5;
z = (- r) + (r + y1) by A65, A66, A1, A67, TARSKI:def 1;
then z = ((- r) + r) + y1 by A2, A8, XXREAL_3:30;
then z = 0. + y1 by XXREAL_3:7;
hence z in Y by A67, XXREAL_3:4; :: thesis: verum

end;

then (- X) + (X + Y) c= Y by TARSKI:def 3;
then A6: Y = (- X) + (X + Y) by A64, XBOOLE_0:def 10;
sup Y <= (sup (X + Y)) + (sup (- X)) by A6, SUPINF_2:26;
then sup Y <= (sup (X + Y)) + (- (inf X)) by SUPINF_2:33;
then sup Y <= (sup (X + Y)) - r by A1, XXREAL_2:13;
then r + (sup Y) <= sup (X + Y) by A2, XXREAL_3:68;
then (sup X) + (sup Y) <= sup (X + Y) by A1, XXREAL_2:11;
hence sup (X + Y) = (sup X) + (sup Y) by A5, XXREAL_0:1; :: thesis: verum