for T being non empty TopSpace
for Z being non empty SubSpace of T
for t being Point of T
for z being Point of Z
for N being open a_neighborhood of t
for M being Subset of Z st t = z & M = N /\ ([#] Z) holds
M is open a_neighborhood of z