theorem Th8: :: UNIFORM2:7

for US being non void UniformSpaceStr holds
( US is axiom_U1 iff for S being Element of the entourages of US ex R being total reflexive Relation of the carrier of US st R = S )