for G being TopologicaladdGroup
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