for US being non empty upper cap-closed axiom_U1 UniformSpaceStr
for x being Element of US holds Neighborhood x is Filter of the carrier of US