let D be non empty bounded_below Subset of REAL ; :: thesis: inf D = inf (Cl D)
A1: inf (Cl D) <= inf D by PSCOMP_1:33, SEQ_4:64;
A2: for p being real number st p in D holds
p >= inf (Cl D)

proof

let p be real number ; :: thesis: ( p in D implies p >= inf (Cl D) )
assume p in D ; :: thesis: p >= inf (Cl D)
then inf D <= p by SEQ_4:def 5;
hence p >= inf (Cl D) by A1, XXREAL_0:2; :: thesis: verum

end;

for q being real number st ( for p being real number st p in D holds
p >= q ) holds
inf (Cl D) >= q

proof

let q be real number ; :: thesis: ( ( for p being real number st p in D holds
p >= q ) implies inf (Cl D) >= q )
assume A3: for p being real number st p in D holds
p >= q ; :: thesis: inf (Cl D) >= q
for p being real number st p in Cl D holds
p >= q

proof

let p be real number ; :: thesis: ( p in Cl D implies p >= q )
assume p in Cl D ; :: thesis: p >= q
then consider s being Real_Sequence such that
A4: rng s c= D and
A5: ( s is convergent & lim s = p ) by PSCOMP_1:39;
for n being Element of NAT holds s . n >= q

proof

let n be Element of NAT ; :: thesis: s . n >= q
dom s = NAT by FUNCT_2:def 1;
then s . n in rng s by FUNCT_1:def 5;
hence s . n >= q by A3, A4; :: thesis: verum

end;

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

end;

hence inf (Cl D) >= q by SEQ_4:60; :: thesis: verum

end;

hence inf D = inf (Cl D) by A2, SEQ_4:61; :: thesis: verum