theorem Th9: :: UNIFORM2:9

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_in the carrier of US ) ) holds
US is axiom_U2