let A be real-membered set ; :: thesis: for x being Real
for y being R_eal st x = y holds
sup (x ++ A) = y + (sup A)
let x be Real; :: thesis: for y being R_eal st x = y holds
sup (x ++ A) = y + (sup A)
let y be R_eal; :: thesis: ( x = y implies sup (x ++ A) = y + (sup A) )
assume A1: x = y ; :: thesis: sup (x ++ A) = y + (sup A)
A2: for z being UpperBound of x ++ A holds y + (sup A) <= z

proof

let z be UpperBound of x ++ A; :: thesis: y + (sup A) <= z
reconsider zz = z as R_eal by XXREAL_0:def 1;
zz - y is UpperBound of A

proof

let u be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not u in A or u <= zz - y )
reconsider uu = u as R_eal by XXREAL_0:def 1;
assume A3: u in A ; :: thesis: u <= zz - y
then reconsider u1 = u as Real ;
y + uu = x + u1 by A1, XXREAL_3:def 2;
then y + uu in x ++ A by A3, Lm1;
then y + uu <= z by XXREAL_2:def 1;
hence u <= zz - y by A1, XXREAL_3:45; :: thesis: verum

end;

then sup A <= zz - y by XXREAL_2:def 3;
hence y + (sup A) <= z by A1, XXREAL_3:45; :: thesis: verum

end;

y + (sup A) is UpperBound of x ++ A

proof

let z be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not z in x ++ A or z <= y + (sup A) )
assume z in x ++ A ; :: thesis: z <= y + (sup A)
then consider a being Real such that
A4: a in A and
A5: z = x + a by Lm1;
reconsider b = a as R_eal by XXREAL_0:def 1;
A6: a <= sup A by A4, XXREAL_2:4;
ex a, c being Complex st
( y = a & b = c & y + b = a + c ) by A1, XXREAL_3:def 2;
hence z <= y + (sup A) by A1, A5, A6, XXREAL_3:36; :: thesis: verum

end;

hence sup (x ++ A) = y + (sup A) by A2, XXREAL_2:def 3; :: thesis: verum