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

per cases ( M is empty or not M is empty ) ;

suppose M is empty ; :: thesis: equ_rel r c= R

hence equ_rel r c= R ; :: thesis: verum

end;

suppose not M is empty ; :: 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 )
assume A2: X in equ_rel r ; :: thesis: 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 R by A2, SETFAM_1:def 1; :: thesis: verum

end;

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

end;

end;