:: deftheorem Def5 defines fam_class TAXONOM1:def 5 :
for X being non empty set
for f being PartFunc of [:X,X:],REAL
for b₃ being Subset of (PARTITIONS X) holds
( b₃ = fam_class f iff for x being object holds
( x in b₃ iff ex a being non negative Real ex R being Equivalence_Relation of X st
( R = (low_toler (f,a)) [*] & Class R = x ) ) );