let X be set ; :: thesis: for R being Equivalence_Relation of X holds RelStr2UniformSpaceStr (UniformSpaceStr2RelStr (uniformity_induced_by R)) = uniformity_induced_by R
let R be Equivalence_Relation of X; :: thesis: RelStr2UniformSpaceStr (UniformSpaceStr2RelStr (uniformity_induced_by R)) = uniformity_induced_by R
( the carrier of (RelStr2UniformSpaceStr (UniformSpaceStr2RelStr (uniformity_induced_by R))) = the carrier of (uniformity_induced_by R) & the entourages of (RelStr2UniformSpaceStr (UniformSpaceStr2RelStr (uniformity_induced_by R))) = rho (meet the entourages of (uniformity_induced_by R)) ) ;
hence RelStr2UniformSpaceStr (UniformSpaceStr2RelStr (uniformity_induced_by R)) = uniformity_induced_by R by Th28; :: thesis: verum