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
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in equ_rel r or 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 ( not X in equ_rel r or X in R ) by SETFAM_1:def 1; :: thesis: verum