set X = { R where R is compatible Equivalence_Relation of : for i being set
for v, w being Element of st i in dom r & r . i = [v,w] holds
v in Class R,w } ;
for v, v', w, w' being Element of st v in Class (equ_rel r),v' & w in Class (equ_rel r),w' holds
v * w in Class (equ_rel r),(v' * w')

proof

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

per cases ( { R where R is compatible Equivalence_Relation of : for i being set
for v, w being Element of st i in dom r & r . i = [v,w] holds
v in Class R,w } = {} or { R where R is compatible Equivalence_Relation of : for i being set
for v, w being Element of st i in dom r & r . i = [v,w] holds
v in Class R,w } <> {} ) ;

suppose { R where R is compatible Equivalence_Relation of : for i being set
for v, w being Element of st i in dom r & r . i = [v,w] holds
v in Class R,w } = {} ; :: thesis: v * w in Class (equ_rel r),(v' * w')

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

end;

suppose A3: { R where R is compatible Equivalence_Relation of : for i being set
for v, w being Element of st i in dom r & r . i = [v,w] holds
v in Class R,w } <> {} ; :: thesis: v * w in Class (equ_rel r),(v' * w')

for Y being set st Y in { R where R is compatible Equivalence_Relation of : for i being set
for v, w being Element of st i in dom r & r . i = [v,w] holds
v in Class R,w } holds
[(v' * w'),(v * w)] in Y

proof

let Y be set ; :: thesis: ( Y in { R where R is compatible Equivalence_Relation of : for i being set
for v, w being Element of st i in dom r & r . i = [v,w] holds
v in Class R,w } implies [(v' * w'),(v * w)] in Y )
assume A4: Y in { R where R is compatible Equivalence_Relation of : for i being set
for v, w being Element of st i in dom r & r . i = [v,w] holds
v in Class R,w } ; :: thesis: [(v' * w'),(v * w)] in Y
then consider R being compatible Equivalence_Relation of such that
A5: ( Y = R & ( for i being set
for v, w being Element of st i in dom r & r . i = [v,w] holds
v in Class R,w ) ) ;
[v',v] in Y by A1, A4, SETFAM_1:def 1;
then A6: v in Class R,v' by A5, EQREL_1:26;
[w',w] in Y by A2, A4, SETFAM_1:def 1;
then A7: w in Class R,w' by A5, EQREL_1:26;
v * w in Class R,(v' * w') by A6, A7, Def4;
hence [(v' * w'),(v * w)] in Y by A5, EQREL_1:26; :: thesis: verum

end;

then [(v' * w'),(v * w)] in meet { R where R is compatible Equivalence_Relation of : for i being set
for v, w being Element of 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),(v' * w') by EQREL_1:26; :: thesis: verum

end;

end;

end;

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