for SUS being non empty axiom_U1 UniformSpaceStr
for x being Element of the carrier of SUS
for V being Element of the entourages of SUS holds
( Neighborhood (V,x) = V .: {x} & Neighborhood (V,x) = rng (V | {x}) & Neighborhood (V,x) = Im (V,x) & Neighborhood (V,x) = Class (V,x) & Neighborhood (V,x) = neighbourhood (,) )