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:18;
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:18;

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:18;
[w9,w] in Y by A2, A4, SETFAM_1:def 1;
then w in Class (R,w9) by A5, EQREL_1:18;
then v * w in Class (R,(v9 * w9)) by A6, Def3;
hence [(v9 * w9),(v * w)] in Y by A5, EQREL_1:18; :: 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:18; :: thesis: verum

end;

end;

end;

hence equ_rel r is compatible ; :: thesis: verum