theorem :: MEASURE6:64
for X being Subset of REAL
for r3 being Real st r3 in Cl X holds
ex seq being Real_Sequence st
( rng seq c= X & seq is convergent & lim seq = r3 )