let T be UnContinuous TopGroup; :: 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 = inverse_op T as Function of T,T ;
( f . a = a " & f is continuous ) by Def7, GROUP_1:def 6;
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 GROUP_1:def 6, TOPS_1:16;
then g " in f .: H by A3, FUNCT_2:35;
hence x in W by A1, A2; :: thesis: verum