:: deftheorem Def1 defines Cl ASCOLI:def 1 :
for X being non empty MetrSpace
for Y, b₃ being Subset of X holds
( b₃ = Cl Y iff ex Z being Subset of (TopSpaceMetr X) st
( Z = Y & b₃ = Cl Z ) );