let X be set ; :: thesis: for SFXX being Subset-Family of [:X,X:] st SFXX <> {} & ( for Y being set st Y in SFXX holds

Y is Equivalence_Relation of X ) holds

meet SFXX is Equivalence_Relation of X

let SFXX be Subset-Family of [:X,X:]; :: thesis: ( SFXX <> {} & ( for Y being set st Y in SFXX holds

Y is Equivalence_Relation of X ) implies meet SFXX is Equivalence_Relation of X )

assume that

A1: SFXX <> {} and

A2: for Y being set st Y in SFXX holds

Y is Equivalence_Relation of X ; :: thesis: meet SFXX is Equivalence_Relation of X

reconsider XX = meet SFXX as Relation of X ;

A3: XX is_symmetric_in X

hence meet SFXX is Equivalence_Relation of X by A3, A5, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum

Y is Equivalence_Relation of X ) holds

meet SFXX is Equivalence_Relation of X

let SFXX be Subset-Family of [:X,X:]; :: thesis: ( SFXX <> {} & ( for Y being set st Y in SFXX holds

Y is Equivalence_Relation of X ) implies meet SFXX is Equivalence_Relation of X )

assume that

A1: SFXX <> {} and

A2: for Y being set st Y in SFXX holds

Y is Equivalence_Relation of X ; :: thesis: meet SFXX is Equivalence_Relation of X

reconsider XX = meet SFXX as Relation of X ;

A3: XX is_symmetric_in X

proof

A5:
XX is_transitive_in X
let x be object ; :: according to RELAT_2:def 3 :: thesis: for b_{1} being object holds

( not x in X or not b_{1} in X or not [x,b_{1}] in XX or [b_{1},x] in XX )

let y be object ; :: thesis: ( not x in X or not y in X or not [x,y] in XX or [y,x] in XX )

assume that

x in X and

y in X and

A4: [x,y] in XX ; :: thesis: [y,x] in XX

end;( not x in X or not b

let y be object ; :: thesis: ( not x in X or not y in X or not [x,y] in XX or [y,x] in XX )

assume that

x in X and

y in X and

A4: [x,y] in XX ; :: thesis: [y,x] in XX

now :: thesis: for Y being set st Y in SFXX holds

[y,x] in Y

hence
[y,x] in XX
by A1, SETFAM_1:def 1; :: thesis: verum[y,x] in Y

let Y be set ; :: thesis: ( Y in SFXX implies [y,x] in Y )

assume Y in SFXX ; :: thesis: [y,x] in Y

then ( Y is Equivalence_Relation of X & [x,y] in Y ) by A2, A4, SETFAM_1:def 1;

hence [y,x] in Y by Th6; :: thesis: verum

end;assume Y in SFXX ; :: thesis: [y,x] in Y

then ( Y is Equivalence_Relation of X & [x,y] in Y ) by A2, A4, SETFAM_1:def 1;

hence [y,x] in Y by Th6; :: thesis: verum

proof

XX is_reflexive_in X
let x be object ; :: according to RELAT_2:def 8 :: thesis: for b_{1}, b_{2} being object holds

( not x in X or not b_{1} in X or not b_{2} in X or not [x,b_{1}] in XX or not [b_{1},b_{2}] in XX or [x,b_{2}] in XX )

let y, z be object ; :: thesis: ( not x in X or not y in X or not z in X or not [x,y] in XX or not [y,z] in XX or [x,z] in XX )

assume that

x in X and

y in X and

z in X and

A6: [x,y] in XX and

A7: [y,z] in XX ; :: thesis: [x,z] in XX

end;( not x in X or not b

let y, z be object ; :: thesis: ( not x in X or not y in X or not z in X or not [x,y] in XX or not [y,z] in XX or [x,z] in XX )

assume that

x in X and

y in X and

z in X and

A6: [x,y] in XX and

A7: [y,z] in XX ; :: thesis: [x,z] in XX

now :: thesis: for Y being set st Y in SFXX holds

[x,z] in Y

hence
[x,z] in XX
by A1, SETFAM_1:def 1; :: thesis: verum[x,z] in Y

let Y be set ; :: thesis: ( Y in SFXX implies [x,z] in Y )

assume A8: Y in SFXX ; :: thesis: [x,z] in Y

then A9: [y,z] in Y by A7, SETFAM_1:def 1;

( Y is Equivalence_Relation of X & [x,y] in Y ) by A2, A6, A8, SETFAM_1:def 1;

hence [x,z] in Y by A9, Th7; :: thesis: verum

end;assume A8: Y in SFXX ; :: thesis: [x,z] in Y

then A9: [y,z] in Y by A7, SETFAM_1:def 1;

( Y is Equivalence_Relation of X & [x,y] in Y ) by A2, A6, A8, SETFAM_1:def 1;

hence [x,z] in Y by A9, Th7; :: thesis: verum

proof

then
( field XX = X & dom XX = X )
by ORDERS_1:13;
let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in XX )

assume A10: x in X ; :: thesis: [x,x] in XX

for Y being set st Y in SFXX holds

[x,x] in Y

end;assume A10: x in X ; :: thesis: [x,x] in XX

for Y being set st Y in SFXX holds

[x,x] in Y

proof

hence
[x,x] in XX
by A1, SETFAM_1:def 1; :: thesis: verum
let Y be set ; :: thesis: ( Y in SFXX implies [x,x] in Y )

assume Y in SFXX ; :: thesis: [x,x] in Y

then Y is Equivalence_Relation of X by A2;

hence [x,x] in Y by A10, Th5; :: thesis: verum

end;assume Y in SFXX ; :: thesis: [x,x] in Y

then Y is Equivalence_Relation of X by A2;

hence [x,x] in Y by A10, Th5; :: thesis: verum

hence meet SFXX is Equivalence_Relation of X by A3, A5, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum