let X be set ; :: thesis: for R being Relation of X ex EqR being Equivalence_Relation of X st

( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

EqR c= EqR2 ) )

let R be Relation of X; :: thesis: ex EqR being Equivalence_Relation of X st

( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

EqR c= EqR2 ) )

defpred S_{1}[ set ] means ( $1 is Equivalence_Relation of X & R c= $1 );

consider F being Subset-Family of [:X,X:] such that

A1: for AX being Subset of [:X,X:] holds

( AX in F iff S_{1}[AX] )
from SUBSET_1:sch 3();

R c= nabla X ;

then A2: F <> {} by A1;

for Y being set st Y in F holds

Y is Equivalence_Relation of X by A1;

then reconsider EqR = meet F as Equivalence_Relation of X by A2, Th11;

A3: for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

EqR c= EqR2 by A1, SETFAM_1:3;

take EqR ; :: thesis: ( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

EqR c= EqR2 ) )

for Y being set st Y in F holds

R c= Y by A1;

hence ( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

EqR c= EqR2 ) ) by A2, A3, SETFAM_1:5; :: thesis: verum

( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

EqR c= EqR2 ) )

let R be Relation of X; :: thesis: ex EqR being Equivalence_Relation of X st

( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

EqR c= EqR2 ) )

defpred S

consider F being Subset-Family of [:X,X:] such that

A1: for AX being Subset of [:X,X:] holds

( AX in F iff S

R c= nabla X ;

then A2: F <> {} by A1;

for Y being set st Y in F holds

Y is Equivalence_Relation of X by A1;

then reconsider EqR = meet F as Equivalence_Relation of X by A2, Th11;

A3: for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

EqR c= EqR2 by A1, SETFAM_1:3;

take EqR ; :: thesis: ( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

EqR c= EqR2 ) )

for Y being set st Y in F holds

R c= Y by A1;

hence ( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds

EqR c= EqR2 ) ) by A2, A3, SETFAM_1:5; :: thesis: verum