for T being UnContinuous TopGroup
for a being Element of T
for W being a_neighborhood of a " ex A being open a_neighborhood of a st A " c= W