theorem Th40: :: GROUP_1A:358

for T being TopologicaladdGroup
for a, b being Element of T
for W being a_neighborhood of a + (- b) ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A + (- B) c= W