let T be UnContinuous TopaddGroup; :: thesis: for a being Element of T
for W being a_neighborhood of - a ex A being open a_neighborhood of a st - A c= W
let a be Element of T; :: thesis: for W being a_neighborhood of - a ex A being open a_neighborhood of a st - A c= W
let W be a_neighborhood of - a; :: thesis: ex A being open a_neighborhood of a st - A c= W
reconsider f = add_inverse T as Function of T,T ;
( f . a = - a & f is continuous ) by Def7, Def6;
then consider H being a_neighborhood of a such that
A1: f .: H c= W by BORSUK_1:def 1;
a in Int (Int H) by CONNSP_2:def 1;
then reconsider A = Int H as open a_neighborhood of a by CONNSP_2:def 1;
take A ; :: thesis: - A c= W
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in - A or x in W )
assume x in - A ; :: thesis: x in W
then consider g being Element of T such that
A2: x = - g and
A3: g in A ;
( Int H c= H & f . g = - g ) by Def6, TOPS_1:16;
then - g in f .: H by A3, FUNCT_2:35;
hence x in W by A1, A2; :: thesis: verum