for US being UniformSpaceStr st US is axiom_U2 holds
for S being Element of the entourages of US
for x, y being Element of US st [x,y] in S holds
[y,x] in union the entourages of US