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_reflexive_in X

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in XX )
assume A4: x in X ; :: thesis: [x,x] in XX
for Y being set st Y in SFXX holds
[x,x] in Y

proof

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 A4, Th11; :: thesis: verum

end;

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

end;

A5: XX is_symmetric_in X

proof

let x be set ; :: according to RELAT_2:def 3 :: thesis: for b₁ being set holds
( not x in X or not b₁ in X or not [x,b₁] in XX or [b₁,x] in XX )
let y be set ; :: thesis: ( not x in X or not y in X or not [x,y] in XX or [y,x] in XX )
assume A6: ( x in X & y in X & [x,y] in XX ) ; :: thesis: [y,x] in XX

now

let Y be set ; :: thesis: ( Y in SFXX implies [y,x] in Y )
assume A7: Y in SFXX ; :: thesis: [y,x] in Y
then A8: Y is Equivalence_Relation of X by A2;
[x,y] in Y by A6, A7, SETFAM_1:def 1;
hence [y,x] in Y by A8, Th12; :: thesis: verum

end;

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

end;

A9: XX is_transitive_in X

proof

let x be set ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being set holds
( not x in X or not b₁ in X or not b₂ in X or not [x,b₁] in XX or not [b₁,b₂] in XX or [x,b₂] in XX )
let y, z be set ; :: 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 A10: ( x in X & y in X & z in X & [x,y] in XX & [y,z] in XX ) ; :: thesis: [x,z] in XX

now

let Y be set ; :: thesis: ( Y in SFXX implies [x,z] in Y )
assume A11: Y in SFXX ; :: thesis: [x,z] in Y
then A12: Y is Equivalence_Relation of X by A2;
( [x,y] in Y & [y,z] in Y ) by A10, A11, SETFAM_1:def 1;
hence [x,z] in Y by A12, Th13; :: thesis: verum

end;

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

end;

A13: field XX = X by A3, ORDERS_1:98;
dom XX = X by A3, ORDERS_1:98;
hence meet SFXX is Equivalence_Relation of X by A5, A9, A13, PARTFUN1:def 4, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum