consider p being real number such that
A1: for r being real number st r in D holds
p <= r by SEQ_4:def 2;
take p ; :: according to SEQ_4:def 2 :: thesis: for b₁ being set holds
( not b₁ in Cl D or p <= b₁ )
let r be real number ; :: 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
A2: rng s c= D and
A3: s is convergent and
A4: lim s = r by PSCOMP_1:39;
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 p <= r by A3, A4, PREPOWER:2; :: thesis: verum