theorem Th8: :: ASCOLI:8

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