let T be TopaddGroup; :: thesis: ( ( for a being Element of T
for W being a_neighborhood of - a ex A being a_neighborhood of a st - A c= W ) implies T is UnContinuous )
assume A1: for a being Element of T
for W being a_neighborhood of - a ex A being a_neighborhood of a st - A c= W ; :: thesis: T is UnContinuous
set f = add_inverse T;
for W being Point of T
for G being a_neighborhood of (add_inverse T) . W ex H being a_neighborhood of W st (add_inverse T) .: H c= G
proof
let a be Point of T; :: thesis: for G being a_neighborhood of (add_inverse T) . a ex H being a_neighborhood of a st (add_inverse T) .: H c= G
let G be a_neighborhood of (add_inverse T) . a; :: thesis: ex H being a_neighborhood of a st (add_inverse T) .: H c= G
(add_inverse T) . a = - a by Def6;
then consider A being a_neighborhood of a such that
A2: - A c= G by A1;
take A ; :: thesis: (add_inverse T) .: A c= G
thus (add_inverse T) .: A c= G by A2, Th9; :: thesis: verum
end;
hence add_inverse T is continuous by BORSUK_1:def 1; :: according to GROUP_1A:def 46 :: thesis: verum