for T being non empty TopSpace
for p being Point of T
for P being non empty Subset of T st p in P holds
for Q being a_neighborhood of p
for p9 being Point of (T | P)
for Q9 being Subset of (T | P) st Q9 = Q /\ P & p9 = p holds
Q9 is a_neighborhood of p9