theorem Th4: :: CONNSP_2:4

for X being non empty TopSpace
for U1 being Subset of X
for x being Point of X st U1 is a_neighborhood of x holds
x in U1