for G being UnContinuous TopaddGroup
for a being Point of G
for A being a_neighborhood of a holds - A is a_neighborhood of - a