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