:: deftheorem defines system_left_uniformity UNIFORM3:def 7 :
for TG being TopologicalGroup holds system_left_uniformity TG = { (element_left_uniformity U) where U is a_neighborhood of 1_ TG : verum } ;