for USS being non empty cap-closed axiom_U1 UniformSpaceStr
for x being Element of USS
for V, W being Element of the entourages of USS holds (Neighborhood (V,x)) /\ (Neighborhood (W,x)) = Neighborhood ((V /\ W),x)