let G be UnContinuous TopGroup; :: thesis: for a being Point of G
for A being a_neighborhood of a holds A " is a_neighborhood of a "
let a be Point of G; :: thesis: for A being a_neighborhood of a holds A " is a_neighborhood of a "
let A be a_neighborhood of a; :: thesis: A " is a_neighborhood of a "
a in Int A by CONNSP_2:def 1;
then consider Q being Subset of G such that
A1: Q is open and
A2: ( Q c= A & a in Q ) by TOPS_1:22;
( Q " c= A " & a " in Q " ) by A2, Th8;
hence a " in Int (A ") by A1, TOPS_1:22; :: according to CONNSP_2:def 1 :: thesis: verum