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