:: deftheorem defines right_uniformity UNIFORM3:def 11 :
for TG being TopologicalGroup holds right_uniformity TG = UniformSpaceStr(# the carrier of TG,<.(system_right_uniformity TG).] #);