theorem Th3: :: ALGSTR_4:3

for M being multMagma
for r being Relators of M
for R being compatible Equivalence_Relation of M st ( 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) ) holds
equ_rel r c= R