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