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 set 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 set ; :: 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, ZFMISC_1:113;
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= {{} } by TARSKI:def 3;
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:39;
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:10, SETFAM_1:11, 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 EQREL_1:34, A3;
hence v in Class (nabla the carrier of M),w by A3, SUBSET_1:def 2; :: thesis: verum

end;

then A5: 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 set 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 set ; :: 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
A6: ( 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 A6; :: 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
A7: ( 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 A7; :: 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 A5, EQREL_1:19; :: thesis: verum

end;

end;