theorem :: UNIFORM3:52

for X being non empty set
for R being Equivalence_Relation of X holds TopSpace_induced_by (@ (uniformity_induced_by R)) = partition_topology (Class R)