:: deftheorem defines NeighborhoodSystem YELLOW19:def 1 :
for T being non empty TopSpace
for x being Point of T holds NeighborhoodSystem x = { A where A is a_neighborhood of x : verum } ;