:: deftheorem defines system_right_uniformity UNIFORM3:def 16 :
for TG being TopaddGroup holds system_right_uniformity TG = { (element_right_uniformity U) where U is a_neighborhood of 0_ TG : verum } ;