:: deftheorem Def6 defines EqClass EQREL_1:def 6 :
for X being non empty set
for x being Element of X
for S1 being a_partition of X
for b₄ being Subset of X holds
( b₄ = EqClass (x,S1) iff ( x in b₄ & b₄ in S1 ) );