for T being non empty TopSpace
for p being Point of T
for x, y being Element of (OpenNeighborhoods p) holds
( x <= y iff y c= x )