theorem :: UNIFORM3:28

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