:: deftheorem defines element_right_uniformity UNIFORM3:def 9 :
for G being TopologicalGroup
for U being a_neighborhood of 1_ G holds element_right_uniformity U = { [x,y] where x, y is Element of G : y * (x ") in U } ;