theorem :: UNIFORM3:23

for MS being PseudoMetricSpace holds TopSpace_induced_by (uniformity_induced_by MS) = TopSpaceMetr MS