theorem :: GROUP_1A:359

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