for USS being non empty axiom_U1 UniformSpaceStr
for x being Element of the carrier of USS
for V being Element of the entourages of USS holds x in Neighborhood (V,x)