set X = { 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 } ;
for v, v9, w, w9 being Element of M st v in Class (equ_rel r),v9 & w in Class (equ_rel r),w9 holds
v * w in Class (equ_rel r),(v9 * w9)

proof

let v, v9, w, w9 be Element of M; :: thesis: ( v in Class (equ_rel r),v9 & w in Class (equ_rel r),w9 implies v * w in Class (equ_rel r),(v9 * w9) )
assume v in Class (equ_rel r),v9 ; :: thesis: ( not w in Class (equ_rel r),w9 or v * w in Class (equ_rel r),(v9 * w9) )
then A1: [v9,v] in equ_rel r by EQREL_1:26;
assume w in Class (equ_rel r),w9 ; :: thesis: v * w in Class (equ_rel r),(v9 * w9)
then A2: [w9,w] in equ_rel r by EQREL_1:26;

per cases ( { 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 } = {} or { 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 } <> {} ) ;

suppose { 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 } = {} ; :: thesis: v * w in Class (equ_rel r),(v9 * w9)

hence v * w in Class (equ_rel r),(v9 * w9) by A1, SETFAM_1:def 1; :: thesis: verum

end;

suppose A3: { 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 } <> {} ; :: thesis: v * w in Class (equ_rel r),(v9 * w9)

for Y being set st Y in { 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 } holds
[(v9 * w9),(v * w)] in Y

proof

let Y be set ; :: thesis: ( Y in { 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 } implies [(v9 * w9),(v * w)] in Y )
assume A4: Y in { 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 } ; :: thesis: [(v9 * w9),(v * w)] in Y
then consider R being compatible Equivalence_Relation of M such that
A5: ( Y = R & ( 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 ) ) ;
[v9,v] in Y by A1, A4, SETFAM_1:def 1;
then A6: v in Class R,v9 by A5, EQREL_1:26;
[w9,w] in Y by A2, A4, SETFAM_1:def 1;
then w in Class R,w9 by A5, EQREL_1:26;
then v * w in Class R,(v9 * w9) by A6, Def4;
hence [(v9 * w9),(v * w)] in Y by A5, EQREL_1:26; :: thesis: verum

end;

then [(v9 * w9),(v * w)] in 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 } by A3, SETFAM_1:def 1;
hence v * w in Class (equ_rel r),(v9 * w9) by EQREL_1:26; :: thesis: verum

end;

end;

end;

hence equ_rel r is compatible by Def4; :: thesis: verum