for G being TopologicalGroup
for a being Point of G
for A being a_neighborhood of a * (a ") ex B being open a_neighborhood of a st B * (B ") c= A