:: deftheorem defines Neighborhood UNIFORM2:def 13 :
for USS being non empty axiom_U1 UniformSpaceStr
for x being Point of USS holds Neighborhood x = { (Neighborhood (V,x)) where V is Element of the entourages of USS : verum } ;