:: deftheorem defines OpenNeighborhoods YELLOW_6:def 14 :
for T being non empty TopSpace
for p being Point of T holds OpenNeighborhoods p = (InclPoset { V where V is Subset of T : ( p in V & V is open ) } ) ~ ;