theorem PRETOPC18: :: NORMSP_3:4

for X being RealNormSpace
for Z being Subset of X holds Z c= Cl Z