let T be TopaddGroup; :: thesis: ( ( 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 ) implies T is TopologicaladdGroup )
assume A1: 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 ; :: thesis: T is TopologicaladdGroup
A2: for a being Element of T
for W being a_neighborhood of - a ex A being a_neighborhood of a st - A c= W

proof

let a be Element of T; :: thesis: for W being a_neighborhood of - a ex A being a_neighborhood of a st - A c= W
let W be a_neighborhood of - a; :: thesis: ex A being a_neighborhood of a st - A c= W
W is a_neighborhood of (0_ T) + (- a) by Def4;
then consider A being a_neighborhood of 0_ T, B being a_neighborhood of a such that
A3: A + (- B) c= W by A1;
take B ; :: thesis: - B c= W
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in - B or x in W )
assume A4: x in - B ; :: thesis: x in W
then consider g being Element of T such that
A5: x = - g and
g in B ;
0_ T in A by CONNSP_2:4;
then (0_ T) + (- g) in A + (- B) by A4, A5;
then - g in A + (- B) by Def4;
hence x in W by A3, A5; :: thesis: verum

end;

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

proof

let a, b be Element of T; :: thesis: 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
let W be a_neighborhood of a + b; :: thesis: ex A being a_neighborhood of a ex B being a_neighborhood of b st A + B c= W
W is a_neighborhood of a + (- (- b)) ;
then consider A being a_neighborhood of a, B being a_neighborhood of - b such that
A6: A + (- B) c= W by A1;
consider B1 being a_neighborhood of b such that
A7: - B1 c= B by A2;
take A ; :: thesis: ex B being a_neighborhood of b st A + B c= W
take B1 ; :: thesis: A + B1 c= W
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + B1 or x in W )
assume x in A + B1 ; :: thesis: x in W
then consider g, h being Element of T such that
A8: ( x = g + h & g in A ) and
A9: h in B1 ;
- h in - B1 by A9;
then h in - B by A7, Th7;
then x in A + (- B) by A8;
hence x in W by A6; :: thesis: verum

end;

hence T is TopologicaladdGroup by A2, ThW37, Th39; :: thesis: verum