theorem :: TOPGRP_1:42

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