for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for x being Point of (X1 union X2)
for x1 being Point of X1
for x2 being Point of X2 st x1 = x & x2 = x holds
for A1 being a_neighborhood of x1
for A2 being a_neighborhood of x2 ex A being a_neighborhood of x st A c= A1 \/ A2