theorem Th21: :: WAYBEL_9:21

for T being non empty TopSpace
for p being Point of T
for A being Element of (OpenNeighborhoods p) holds A is a_neighborhood of p