:: deftheorem Def2 defines MSEquivalence_Relation-like MSUALG_4:def 2 :
for I being set
for A being ManySortedSet of I
for IT being ManySortedRelation of A holds
( IT is MSEquivalence_Relation-like iff for i being set
for R being Relation of (A . i) st i in I & IT . i = R holds
R is Equivalence_Relation of (A . i) );