theorem Th54: :: GROUP_1A:372

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