theorem :: COMPL_SP:19

for M being non empty MetrSpace st M is complete holds
for A being non empty Subset of M
for A9 being Subset of (TopSpaceMetr M) st A = A9 holds
( M | A is complete iff A9 is closed )