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

let q be Real; :: thesis:
assume A2: for p being Real st p in D holds
p >= q ; :: thesis:
for p being Real st p in Cl D holds
p >= q

let p be Real; :: thesis:
assume p in Cl D ; :: thesis:
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

let n be Nat; :: thesis:
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:

end;

hence p >= q by A4, A5, PREPOWER:1; :: thesis:

end;

hence lower_bound (Cl D) >= q by SEQ_4:43; :: thesis:

end;

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

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

end;

hence lower_bound D = lower_bound (Cl D) by A1, SEQ_4:44; :: thesis: