theorem Th6: :: CONNSP_2:6

for X being non empty TopSpace
for x being Point of X
for U1 being Subset of X holds
( U1 is a_neighborhood of x iff ex V being Subset of X st
( V is open & V c= U1 & x in V ) )