for US being upper UniformSpaceStr
for 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) by Th31;