theorem :: UNIFORM3:64

for X being set
for R being Equivalence_Relation of X holds RelStr2UniformSpaceStr (UniformSpaceStr2RelStr (uniformity_induced_by R)) = uniformity_induced_by R