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

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
A5: x in - X and
A6: y in X + Y and
A7: z = x + y by SUPINF_2:def 5;
consider x1, y1 being R_eal such that
A8: x1 in X and
A9: y1 in Y and
A10: y = x1 + y1 by A6, SUPINF_2:def 5;
- x in - (- X) by A5, SUPINF_2:23;
then - x in X by SUPINF_2:22;
then - x = r by A1, TARSKI:def 1;
then z = (- r) + (r + y1) by A1, 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: (- X) + (X + Y) c= Y by TARSKI:def 3;
A12: r in X by A1, TARSKI:def 1;

now

let z be set ; :: thesis: ( z in Y implies z in (- X) + (X + Y) )
assume A13: z in Y ; :: thesis: z in (- X) + (X + 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 - X by A12, SUPINF_2:def 6;
r + y in X + Y by A12, A13, SUPINF_2:def 5;
hence z in (- X) + (X + Y) by A15, A14, SUPINF_2:def 5; :: thesis: verum

end;

then Y c= (- X) + (X + Y) by TARSKI:def 3;
then Y = (- X) + (X + Y) by A11, XBOOLE_0:def 10;
then inf Y >= (inf (X + Y)) + (inf (- X)) by SUPINF_2:27;
then inf Y >= (inf (X + Y)) + (- (sup X)) by SUPINF_2:32;
then inf Y >= (inf (X + Y)) - r by A1, XXREAL_2:11;
then r + (inf Y) >= inf (X + Y) by A2, XXREAL_3:63;
then A16: (inf X) + (inf Y) >= inf (X + Y) by A1, XXREAL_2:13;
inf (X + Y) >= (inf X) + (inf Y) by SUPINF_2:27;
hence inf (X + Y) = (inf X) + (inf Y) by A16, XXREAL_0:1; :: thesis: verum