theorem Th11: :: UNIFORM3:22

for MS being PseudoMetricSpace holds Family_open_set (FMT_induced_by (uniformity_induced_by MS)) = Family_open_set MS