theorem Th4: :: ASCOLI2:4

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