:: deftheorem defines element_right_uniformity UNIFORM3:def 15 :
for G being TopaddGroup
for U being a_neighborhood of 0_ G holds element_right_uniformity U = { [x,y] where x, y is Element of G : y + (- x) in U } ;