let D be non empty bounded_above Subset of REAL; :: thesis: upper_bound D = upper_bound (Cl D)
A1: for q being Real st ( for p being Real st p in D holds
p <= q ) holds
upper_bound (Cl D) <= q

proof

let q be Real; :: thesis: ( ( for p being Real st p in D holds
p <= q ) implies upper_bound (Cl D) <= q )
assume A2: for p being Real st p in D holds
p <= q ; :: thesis: upper_bound (Cl D) <= q
for p being Real st p in Cl D holds
p <= q

proof

let p be Real; :: thesis: ( p in Cl D implies p <= q )
assume p in Cl D ; :: thesis: p <= q
then consider s being Real_Sequence such that
A3: rng s c= D and
A4: s is convergent and
A5: lim s = p by MEASURE6:64;
for n being Nat holds s . n <= q

proof

let n be Nat; :: thesis: s . n <= q
A6: n in NAT by ORDINAL1:def 12;
dom s = NAT by FUNCT_2:def 1;
then s . n in rng s by A6, FUNCT_1:def 3;
hence s . n <= q by A2, A3; :: thesis: verum

end;

hence p <= q by A4, A5, PREPOWER:2; :: thesis: verum

end;

hence upper_bound (Cl D) <= q by SEQ_4:45; :: thesis: verum

end;

A7: upper_bound (Cl D) >= upper_bound D by MEASURE6:58, SEQ_4:48;
for p being Real st p in D holds
p <= upper_bound (Cl D)

proof

let p be Real; :: thesis: ( p in D implies p <= upper_bound (Cl D) )
assume p in D ; :: thesis: p <= upper_bound (Cl D)
then upper_bound D >= p by SEQ_4:def 1;
hence p <= upper_bound (Cl D) by A7, XXREAL_0:2; :: thesis: verum

end;

hence upper_bound D = upper_bound (Cl D) by A1, SEQ_4:46; :: thesis: verum