for Z being RealNormSpace
for H being non empty Subset of (MetricSpaceNorm Z) st Z is complete holds
(MetricSpaceNorm Z) | (Cl H) is complete