for G being UnContinuous TopGroup
for a being Point of G
for A being a_neighborhood of a holds A " is a_neighborhood of a "