theorem :: UNIFORM3:29

for TG being TopologicalGroup holds the topology of (TopSpace_induced_by (right_uniformity TG)) = the topology of TG