:: deftheorem Def3 defines EqCl MSUALG_5:def 3 :
for I being non empty set
for M being ManySortedSet of I
for R being ManySortedRelation of M
for b₄ being Equivalence_Relation of M holds
( b₄ = EqCl R iff for i being Element of I holds b₄ . i = EqCl (R . i) );