let X be set ; :: thesis: for P being a_partition of X ex EqR being Equivalence_Relation of X st P = Class EqR
let P be a_partition of X; :: thesis: ex EqR being Equivalence_Relation of X st P = Class EqR
A1: ( X <> {} implies ex EqR being Equivalence_Relation of X st P = Class EqR )

proof

defpred S₁[ object , object ] means ex A being Subset of X st
( A in P & $1 in A & $2 in A );
assume X <> {} ; :: thesis: ex EqR being Equivalence_Relation of X st P = Class EqR
A2: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z]

proof

let x, y, z be object ; :: thesis: ( S₁[x,y] & S₁[y,z] implies S₁[x,z] )
given A being Subset of X such that A3: A in P and
A4: ( x in A & y in A ) ; :: thesis: ( not S₁[y,z] or S₁[x,z] )
given B being Subset of X such that A5: B in P and
A6: ( y in B & z in B ) ; :: thesis: S₁[x,z]
( A = B or A misses B ) by A3, A5, Def4;
hence S₁[x,z] by A3, A4, A6, XBOOLE_0:3; :: thesis: verum

end;

A7: union P = X by Def4;
A8: for x being object st x in X holds
S₁[x,x]

proof

let x be object ; :: thesis: ( x in X implies S₁[x,x] )
assume x in X ; :: thesis: S₁[x,x]
then consider Z being set such that
A9: x in Z and
A10: Z in P by A7, TARSKI:def 4;
reconsider A = Z as Subset of X by A10;
take A ; :: thesis: ( A in P & x in A & x in A )
thus ( A in P & x in A & x in A ) by A9, A10; :: thesis: verum

end;

A11: for x, y being object st S₁[x,y] holds
S₁[y,x] ;
consider R being Equivalence_Relation of X such that
A12: for x, y being object holds
( [x,y] in R iff ( x in X & y in X & S₁[x,y] ) ) from EQREL_1:sch 1(A8, A11, A2);
take R ; :: thesis: P = Class R

now :: thesis: for A being Subset of X holds
( A in P iff A in Class R )

let A be Subset of X; :: thesis: ( A in P iff A in Class R )

A13: now :: thesis: ( A in P implies A in Class R )

set x = the Element of A;
assume A14: A in P ; :: thesis: A in Class R
then A15: A <> {} by Def4;
then A16: the Element of A in X by TARSKI:def 3;

now :: thesis: for y being object holds
( y in A iff y in Class (R, the Element of A) )

let y be object ; :: thesis: ( y in A iff y in Class (R, the Element of A) )

A17: now :: thesis: ( y in Class (R, the Element of A) implies y in A )

assume y in Class (R, the Element of A) ; :: thesis: y in A
then [y, the Element of A] in R by Th19;
then consider B being Subset of X such that
A18: ( B in P & y in B ) and
A19: the Element of A in B by A12;
A meets B by A15, A19, XBOOLE_0:3;
hence y in A by A14, A18, Def4; :: thesis: verum

end;

now :: thesis: ( y in A implies y in Class (R, the Element of A) )

assume y in A ; :: thesis: y in Class (R, the Element of A)
then [y, the Element of A] in R by A12, A14, A16;
hence y in Class (R, the Element of A) by Th19; :: thesis: verum

end;

hence ( y in A iff y in Class (R, the Element of A) ) by A17; :: thesis: verum

end;

then A = Class (R, the Element of A) by TARSKI:2;
hence A in Class R by A16, Def3; :: thesis: verum

end;

now :: thesis: ( A in Class R implies A in P )

assume A in Class R ; :: thesis: A in P
then consider x being object such that
A20: x in X and
A21: A = Class (R,x) by Def3;
x in Class (R,x) by A20, Th20;
then [x,x] in R by Th19;
then consider B being Subset of X such that
A22: B in P and
A23: x in B and
x in B by A12;

now :: thesis: for y being object holds
( y in A iff y in B )

let y be object ; :: thesis: ( y in A iff y in B )

A24: now :: thesis: ( y in A implies y in B )

assume y in A ; :: thesis: y in B
then [y,x] in R by A21, Th19;
then consider C being Subset of X such that
A25: ( C in P & y in C ) and
A26: x in C by A12;
B meets C by A23, A26, XBOOLE_0:3;
hence y in B by A22, A25, Def4; :: thesis: verum

end;

now :: thesis: ( y in B implies y in A )

assume y in B ; :: thesis: y in A
then [y,x] in R by A12, A22, A23;
hence y in A by A21, Th19; :: thesis: verum

end;

hence ( y in A iff y in B ) by A24; :: thesis: verum

end;

hence A in P by A22, TARSKI:2; :: thesis: verum

end;

hence ( A in P iff A in Class R ) by A13; :: thesis: verum

end;

hence P = Class R by SETFAM_1:31; :: thesis: verum

end;

( X = {} implies ex EqR being Equivalence_Relation of X st P = Class EqR )

proof

set EqR1 = the Equivalence_Relation of X;
assume A27: X = {} ; :: thesis: ex EqR being Equivalence_Relation of X st P = Class EqR
take the Equivalence_Relation of X ; :: thesis: P = Class the Equivalence_Relation of X
P = {} by A27;
hence P = Class the Equivalence_Relation of X by A27, Th31; :: thesis: verum

end;

hence ex EqR being Equivalence_Relation of X st P = Class EqR by A1; :: thesis: verum