theorem :: NORMSP_3:7

for X being RealNormSpace
for A being Subset of X ex F being Subset-Family of X st
( ( for C being Subset of X holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )