let MS be PseudoMetricSpace; :: thesis: TopSpace_induced_by (uniformity_induced_by MS) = TopSpaceMetr MS
the topology of (FMT2TopSpace (FMT_induced_by (uniformity_induced_by MS))) = Family_open_set (FMT_induced_by (uniformity_induced_by MS)) by FINTOPO7:def 16;
hence TopSpace_induced_by (uniformity_induced_by MS) = TopSpaceMetr MS by FINTOPO7:def 16, Th11; :: thesis: verum