for S, T being non empty TopSpace
for s being Point of S
for t being Point of T
for A being a_neighborhood of s st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & s = t holds
A is a_neighborhood of t