for TG being TopologicalGroup
for V being a_neighborhood of 1_ TG holds V " is a_neighborhood of 1_ TG