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 ;
A1: f . a = a " by GROUP_1:def 7;
f is continuous by Def7;
then consider H being a_neighborhood of a such that
A2: f .: H c= W by A1, BORSUK_1:def 3;
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 set ; :: 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
A4: ( x = g " & g in A ) ;
A5: Int H c= H by TOPS_1:44;
f . g = g " by GROUP_1:def 7;
then g " in f .: H by A4, A5, FUNCT_2:43;
hence x in W by A2, A4; :: thesis: verum