let X be set ; :: thesis: for P being a_partition of X holds P = Class (ERl P)
let P be a_partition of X; :: thesis: P = Class (ERl P)
set R = ERl P;

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

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

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

set x = the Element of A;
assume A14: A in P ; :: thesis: A in Class (ERl P)
then A15: A <> {} by EQREL_1:def 4;
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 ((ERl P), the Element of A) )

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

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

assume y in Class ((ERl P), the Element of A) ; :: thesis: y in A
then [y, the Element of A] in ERl P by EQREL_1:19;
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 Def6;
A meets B by A15, A19, XBOOLE_0:3;
hence y in A by A14, A18, EQREL_1:def 4; :: thesis: verum

end;

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

assume y in A ; :: thesis: y in Class ((ERl P), the Element of A)
then [y, the Element of A] in ERl P by Def6, A14;
hence y in Class ((ERl P), the Element of A) by EQREL_1:19; :: thesis: verum

end;

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

end;

then A = Class ((ERl P), the Element of A) by TARSKI:2;
hence A in Class (ERl P) by A16, EQREL_1:def 3; :: thesis: verum

end;

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

assume A in Class (ERl P) ; :: thesis: A in P
then consider x being object such that
A20: x in X and
A21: A = Class ((ERl P),x) by EQREL_1:def 3;
x in Class ((ERl P),x) by A20, EQREL_1:20;
then [x,x] in ERl P by EQREL_1:19;
then consider B being Subset of X such that
A22: B in P and
A23: x in B and
x in B by Def6;

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 ERl P by A21, EQREL_1:19;
then consider C being Subset of X such that
A25: ( C in P & y in C ) and
A26: x in C by Def6;
B meets C by A23, A26, XBOOLE_0:3;
hence y in B by A22, A25, EQREL_1:def 4; :: thesis: verum

end;

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

assume y in B ; :: thesis: y in A
then [y,x] in ERl P by Def6, A22, A23;
hence y in A by A21, EQREL_1:19; :: 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 (ERl P) ) by A13; :: thesis: verum

end;

hence P = Class (ERl P) by SETFAM_1:31; :: thesis: verum