theorem :: UNIFORM3:62

for X being set
for R being Tolerance of X holds
( uniformity_induced_by R is Semi-UniformSpace & the entourages of (uniformity_induced_by R) = rho R & meet the entourages of (uniformity_induced_by R) = R ) by Th28;