for USS being non empty upper axiom_U1 UniformSpaceStr
for x being Element of the carrier of USS holds Neighborhood x is upper