theorem Th34: :: PCOMPS_1:34

for PM being non empty MetrSpace holds TopSpaceMetr PM is T_2