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 A1: r in REAL ; :: thesis: sup ({r} + Y) = (sup {r}) + (sup Y)
set W = {r} + Y;
A2: - r <> -infty by A1, XXREAL_3:23;
A3: - r <> +infty by A1, XXREAL_3:23;
now :: thesis: for z being object st z in (- {r}) + ({r} + Y) holds
z in Y
let z be object ; :: 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
A4: z = x + y and
A5: x in - {r} and
A6: y in {r} + Y ;
consider x1, y1 being R_eal such that
A7: y = x1 + y1 and
A8: x1 in {r} and
A9: y1 in Y by A6;
- x in - (- {r}) by A5;
then - x in {r} ;
then - x = r by TARSKI:def 1;
then z = (- r) + (r + y1) by A4, A8, A7, TARSKI:def 1;
then z = ((- r) + r) + y1 by A1, A3, A2, XXREAL_3:29;
then z = 0. + y1 by XXREAL_3:7;
hence z in Y by A9, XXREAL_3:4; :: thesis: verum
end;
then A10: (- {r}) + ({r} + Y) c= Y by TARSKI:def 3;
A11: r in {r} by TARSKI:def 1;
now :: thesis: for z being object st z in Y holds
z in (- {r}) + ({r} + Y)
let z be object ; :: thesis: ( z in Y implies z in (- {r}) + ({r} + Y) )
assume A12: z in Y ; :: thesis: z in (- {r}) + ({r} + Y)
then reconsider y = z as Element of ExtREAL ;
(r + y) - r = ((- r) + r) + y by A1, A3, A2, XXREAL_3:29;
then (r + y) - r = 0. + y by XXREAL_3:7;
then A13: y = (r + y) - r by XXREAL_3:4;
A14: - r in - {r} by A11;
r + y in {r} + Y by A11, A12;
hence z in (- {r}) + ({r} + Y) by A14, A13; :: thesis: verum
end;
then Y c= (- {r}) + ({r} + Y) by TARSKI:def 3;
then Y = (- {r}) + ({r} + Y) by A10, XBOOLE_0:def 10;
then sup Y <= (sup ({r} + Y)) + (sup (- {r})) by SUPINF_2:8;
then sup Y <= (sup ({r} + Y)) + (- (inf {r})) by SUPINF_2:15;
then sup Y <= (sup ({r} + Y)) - r by XXREAL_2:13;
then r + (sup Y) <= sup ({r} + Y) by A1, XXREAL_3:57;
then A15: (sup {r}) + (sup Y) <= sup ({r} + Y) by XXREAL_2:11;
sup ({r} + Y) <= (sup {r}) + (sup Y) by SUPINF_2:8;
hence sup ({r} + Y) = (sup {r}) + (sup Y) by A15, XXREAL_0:1; :: thesis: verum