:: deftheorem defines equ_rel ALGSTR_4:def 7 :
for M being multMagma
for r being Relators of M holds equ_rel r = meet { R where R is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class (R,w) } ;