:: deftheorem defines Neighborhood UNIFORM2:def 12 :
for SUS being non empty axiom_U1 UniformSpaceStr
for x being Element of SUS
for V being Element of the entourages of SUS holds Neighborhood (V,x) = { y where y is Element of SUS : [x,y] in V } ;