theorem :: TAXONOM1:25

for X being non empty set
for f being PartFunc of [:X,X:],REAL
for R being Equivalence_Relation of X st R = (low_toler (f,0)) [*] & f is nonnegative & f is Reflexive & f is discerning holds
Class R = SmallestPartition X by Th24;