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) } ;

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

suppose M is empty ; :: thesis: 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) } is Equivalence_Relation of M

then A1: the carrier of M = {} ;
for x being object st x 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
x in {{}}

proof

let x be object ; :: thesis: ( x 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 x in {{}} )
assume x 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: x in {{}}
then consider R being compatible Equivalence_Relation of M such that
A2: ( x = 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) ) ) ;
x is Subset of {} by A2, A1;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

then { 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) } c= {{}} ;
then ( { 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) } = {{}} ) by ZFMISC_1:33;
hence 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) } is Equivalence_Relation of M by A1, OSALG_4:9, SETFAM_1:10, SETFAM_1:def 1; :: thesis: verum

end;

suppose A3: not M is empty ; :: thesis: 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) } is 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 ((nabla the carrier of M),w)

proof

let i be set ; :: thesis: for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class ((nabla the carrier of M),w)
let v, w be Element of M; :: thesis: ( i in dom r & r . i = [v,w] implies v in Class ((nabla the carrier of M),w) )
assume ( i in dom r & r . i = [v,w] ) ; :: thesis: v in Class ((nabla the carrier of M),w)
Class ((nabla the carrier of M),w) = the carrier of M by A3, EQREL_1:26;
hence v in Class ((nabla the carrier of M),w) by A3, SUBSET_1:def 1; :: thesis: verum

end;

then A4: nabla the carrier of M 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) } ;
for x being object st x 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
x in bool [: the carrier of M, the carrier of M:]

proof

let x be object ; :: thesis: ( x 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 x in bool [: the carrier of M, the carrier of M:] )
assume x 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: x in bool [: the carrier of M, the carrier of M:]
then consider R being compatible Equivalence_Relation of M such that
A5: ( x = R & ( for i being set
for x, y being Element of M st i in dom r & r . i = [x,y] holds
x in Class (R,y) ) ) ;
thus x in bool [: the carrier of M, the carrier of M:] by A5; :: thesis: verum

end;

then reconsider 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) } as Subset-Family of [: the carrier of M, the carrier of M:] by TARSKI:def 3;
for Y being set st Y in X holds
Y is Equivalence_Relation of M

proof

let Y be set ; :: thesis: ( Y in X implies Y is Equivalence_Relation of M )
assume Y in X ; :: thesis: Y is Equivalence_Relation of M
then consider R being compatible Equivalence_Relation of M such that
A6: ( 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) ) ) ;
thus Y is Equivalence_Relation of M by A6; :: thesis: verum

end;

hence 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) } is Equivalence_Relation of M by A4, EQREL_1:11; :: thesis: verum

end;

end;