:: deftheorem Def6 defines ERl PARTIT1:def 6 :
for Y being set
for PA being a_partition of Y
for b₃ being Equivalence_Relation of Y holds
( b₃ = ERl PA iff for x1, x2 being object holds
( [x1,x2] in b₃ iff ex A being Subset of Y st
( A in PA & x1 in A & x2 in A ) ) );