let T be TopGroup; :: 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 = inverse_op T;
for W being Point of T
for G being a_neighborhood of (inverse_op T) . W ex H being a_neighborhood of W st (inverse_op T) .: H c= G

proof

let a be Point of T; :: thesis: for G being a_neighborhood of (inverse_op T) . a ex H being a_neighborhood of a st (inverse_op T) .: H c= G
let G be a_neighborhood of (inverse_op T) . a; :: thesis: ex H being a_neighborhood of a st (inverse_op T) .: H c= G
(inverse_op T) . a = a " by GROUP_1:def 6;
then consider A being a_neighborhood of a such that
A2: A " c= G by A1;
take A ; :: thesis: (inverse_op T) .: A c= G
thus (inverse_op T) .: A c= G by A2, Th9; :: thesis: verum

end;

hence inverse_op T is continuous by BORSUK_1:def 1; :: according to TOPGRP_1:def 7 :: thesis: verum