theorem Th9: :: CONNSP_2:9

for X being non empty TopSpace
for B being non empty Subset of X
for x being Point of (X | B)
for A being Subset of (X | B)
for A1 being Subset of X
for x1 being Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds
A1 is a_neighborhood of x1