theorem Th38: :: TOPGRP_1:39

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