theorem Th54: :: TOPGRP_1:55

for G being TopologicalGroup
for a being Point of G
for A being a_neighborhood of a * (a ") ex B being open a_neighborhood of a st B * (B ") c= A