theorem Th53: :: TOPGRP_1:54

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 "