consider p being Real such that
A1: p is LowerBound of D by XXREAL_2:def 9;
A2: for r being Real st r in D holds
p <= r by A1, XXREAL_2:def 2;
take p ; :: according to XXREAL_2:def 9 :: thesis: p is LowerBound of Cl D
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in Cl D or p <= r )
assume r in Cl D ; :: thesis: p <= r
then consider s being Real_Sequence such that
A3: rng s c= D and
A4: s is convergent and
A5: lim s = r by MEASURE6:64;
for n being Nat holds s . n >= p

proof

let n be Nat; :: thesis: s . n >= p
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 >= p by A2, A3; :: thesis: verum

end;

hence p <= r by A4, A5, PREPOWER:1; :: thesis: verum