for T being TopologicalGroup
for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W