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

proof

let x be object ; :: according to RELAT_2:def 3 :: thesis: for b₁ being object holds
( not x in X or not b₁ in X or not [x,b₁] in XX or [b₁,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

now :: thesis: for Y being set st Y in SFXX holds
[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;

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

end;

A5: XX is_transitive_in X

proof

let x be object ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being object 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 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

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;

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

end;

XX is_reflexive_in X

proof

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

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 A10, Th5; :: thesis: verum

end;

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

end;

then ( field XX = X & dom XX = X ) by ORDERS_1:13;
hence meet SFXX is Equivalence_Relation of X by A3, A5, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum