let Y be non empty set ; :: thesis: for PA being a_partition of Y ex RA being Equivalence_Relation of Y st
for x, y being set holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) )
let PA be a_partition of Y; :: thesis: ex RA being Equivalence_Relation of Y st
for x, y being set holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) )
A1: ( union PA = Y & ( for A being Subset of Y st A in PA holds
( A <> {} & ( for B being Subset of Y holds
( not B in PA or A = B or A misses B ) ) ) ) ) by EQREL_1:def 6;
ex RA being Equivalence_Relation of Y st
for x, y being set holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) )

proof

defpred S₁[ set , set ] means ex A being Subset of Y st
( A in PA & $1 in A & $2 in A );
A2: for x being set st x in Y holds
S₁[x,x]

proof

let x be set ; :: thesis: ( x in Y implies S₁[x,x] )
assume x in Y ; :: thesis: S₁[x,x]
then ex Z being set st
( x in Z & Z in PA ) by A1, TARSKI:def 4;
then consider Z being non empty set such that
A3: ( x in Z & Z in PA ) ;
reconsider A = Z as Subset of Y by A3;
take A ; :: thesis: ( A in PA & x in A & x in A )
thus ( A in PA & x in A & x in A ) by A3; :: thesis: verum

end;

A4: for x, y being set st S₁[x,y] holds
S₁[y,x] ;
A5: for x, y, z being set st S₁[x,y] & S₁[y,z] holds
S₁[x,z]

proof

let x, y, z be set ; :: thesis: ( S₁[x,y] & S₁[y,z] implies S₁[x,z] )
given A being Subset of Y such that A6: ( A in PA & x in A & y in A ) ; :: thesis: ( not S₁[y,z] or S₁[x,z] )
given B being Subset of Y such that A7: ( B in PA & y in B & z in B ) ; :: thesis: S₁[x,z]
( A = B or A misses B ) by A6, A7, EQREL_1:def 6;
hence S₁[x,z] by A6, A7, XBOOLE_0:3; :: thesis: verum

end;

consider RA being Equivalence_Relation of Y such that
A8: for x, y being set holds
( [x,y] in RA iff ( x in Y & y in Y & S₁[x,y] ) ) from EQREL_1:sch 1(A2, A4, A5);
take RA ; :: thesis: for x, y being set holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) )
thus for x, y being set holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) ) by A8; :: thesis: verum

end;

hence ex RA being Equivalence_Relation of Y st
for x, y being set holds
( [x,y] in RA iff ex A being Subset of Y st
( A in PA & x in A & y in A ) ) ; :: thesis: verum