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₁[ 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₁[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