theorem Th16: :: HAUSDORF:16

for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M)
for Q being non empty Subset of M st P = Q holds
(TopSpaceMetr M) | P = TopSpaceMetr (M | Q)