let T be TopologicaladdGroup; :: thesis: 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
let a, b be Element of T; :: thesis: 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
let W be a_neighborhood of a + (- b); :: thesis: ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A + (- B) c= W
consider A being open a_neighborhood of a, B being open a_neighborhood of - b such that
A1: A + B c= W by Th36;
consider C being open a_neighborhood of b such that
A2: - C c= B by Th38;
take A ; :: thesis: ex B being open a_neighborhood of b st A + (- B) c= W
take C ; :: thesis: A + (- C) c= W
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + (- C) or x in W )
assume x in A + (- C) ; :: thesis: x in W
then consider g, h being Element of T such that
A3: x = g + h and
A4: g in A and
A5: h in - C ;
consider k being Element of T such that
A6: h = - k and
k in C by A5;
g + (- k) in A + B by A2, A4, A5, A6;
hence x in W by A1, A3, A6; :: thesis: verum