let M be multMagma ; :: thesis: 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
let r be Relators of M; :: thesis: 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
let R be compatible Equivalence_Relation of M; :: thesis: ( ( 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) ) implies equ_rel r c= R )
assume A1: 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) ; :: thesis: equ_rel r c= R
for X being set st X in equ_rel r holds
X in R

proof

let X be set ; :: thesis: ( X in equ_rel r implies X in R )
R in { R9 where R9 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 (R9,w) } by A1;
hence ( X in equ_rel r implies X in R ) by SETFAM_1:def 1; :: thesis: verum

end;

hence equ_rel r c= R by TARSKI:def 3; :: thesis: verum