for US being non void UniformSpaceStr st ( for S being Element of the entourages of US ex R being Relation of the carrier of US st
( S = R & R is symmetric ) ) holds
US is axiom_U2