theorem Th5: :: ASCOLI2:5

for Z being non empty MetrSpace
for H being non empty Subset of Z st Z is complete & Z | H is totally_bounded holds
( Cl H is sequentially_compact & Z | (Cl H) is compact )