:: deftheorem defcl defines Cl NORMSP_3:def 1 :
for X being RealNormSpace
for Y, b₃ being Subset of X holds
( b₃ = Cl Y iff ex Z being Subset of (LinearTopSpaceNorm X) st
( Z = Y & b₃ = Cl Z ) );