theorem Th7: :: UNIFORM2:6

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