for T being non empty TopSpace
for p being Point of T
for x being Subset of T holds
( x in the carrier of (OpenNeighborhoods p) iff ( p in x & x is open ) )