let A be real-membered set ; :: thesis: for x being real number
for y being R_eal st x = y holds
sup (x ++ A) = y + (sup A)
let x be real number ; :: 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 Z: x = y ; :: thesis: sup (x ++ A) = y + (sup A)
A: y + (sup A) is UpperBound of x ++ A

proof

let z be ext-real number ; :: 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
W1: a in A and
W2: z = x + a by Def6;
reconsider b = a as R_eal by XXREAL_0:def 1;
V: ex a, c being complex number st
( y = a & b = c & y + b = a + c ) by Z, XXREAL_3:def 2;
a <= sup A by W1, XXREAL_2:4;
hence z <= y + (sup A) by V, W2, Z, XXREAL_3:38; :: thesis: verum

end;

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 ext-real number ; :: 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 ZZ: u in A ; :: thesis: u <= zz - y
then reconsider u1 = u as Real by XREAL_0:def 1;
u1 in REAL ;
then consider a, b being complex number such that
W1: y = a and
W2: uu = b and
W3: y + uu = a + b by Z, XXREAL_3:def 2;
y + uu = x + u1 by Z, W1, W2, W3;
then y + uu in x ++ A by Def6, ZZ;
then y + uu <= z by XXREAL_2:def 1;
hence u <= zz - y by Z, XXREAL_3:49; :: thesis: verum

end;

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

end;

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