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