theorem Th4: :: UNIFORM3:9

for TG being TopologicalGroup
for e being Element of TG
for V being a_neighborhood of 1_ TG holds {e} * V is a_neighborhood of e