:: deftheorem Def3 defines Neighborhood_System TOPGEN_2:def 3 :
for T being non empty TopSpace
for b₂ being ManySortedSet of T holds
( b₂ is Neighborhood_System of T iff for x being Element of T holds b₂ . x is Basis of x );