consider p being real number such that
B1: p is UpperBound of D by XXREAL_2:def 10;
A1: for r being real number st r in D holds
r <= p by B1, XXREAL_2:def 1;
take p ; :: according to XXREAL_2:def 10 :: thesis: p is UpperBound of Cl D
let r be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not r in Cl D or r <= p )
assume r in Cl D ; :: thesis: r <= p
then consider s being Real_Sequence such that
A2: rng s c= D and
A3: s is convergent and
A4: lim s = r by MEASURE6:100;
for n being Element of NAT holds s . n <= p

proof

let n be Element of NAT ; :: thesis: s . n <= p
dom s = NAT by FUNCT_2:def 1;
then s . n in rng s by FUNCT_1:def 5;
hence s . n <= p by A1, A2; :: thesis: verum

end;

hence r <= p by A3, A4, PREPOWER:3; :: thesis: verum