let G be UnContinuous TopaddGroup; :: 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, ThB8;
hence - a in Int (- A) by A1, TOPS_1:22; :: according to CONNSP_2:def 1 :: thesis: verum