theorem Th31: :: UNIFORM3:60

for US being upper UniformSpaceStr st ex R being Relation of the carrier of US st
( the entourages of US = rho R & meet the entourages of US in the entourages of US ) holds
the entourages of US = rho (meet the entourages of US)