let A be non empty finite set ; :: thesis: for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 & card PA1 = card PA2 holds
PA1 = PA2
let PA1, PA2 be a_partition of A; :: thesis: ( PA1 is_finer_than PA2 & card PA1 = card PA2 implies PA1 = PA2 )
defpred S₁[ set , set ] means $1 c= $2;
assume that
A1: PA1 is_finer_than PA2 and
A2: card PA1 = card PA2 ; :: thesis: PA1 = PA2
A3: for e being set st e in PA1 holds
ex u being set st
( u in PA2 & S₁[e,u] ) by A1, SETFAM_1:def 2;
consider f being Function of PA1,PA2 such that
A4: for e being set st e in PA1 holds
S₁[e,f . e] from FUNCT_2:sch 1(A3);
A5: dom f = PA1 by FUNCT_2:def 1;
A6: PA2 c= rng f

proof

let p2 be set ; :: according to TARSKI:def 3 :: thesis: ( not p2 in PA2 or p2 in rng f )
assume p2 in PA2 ; :: thesis: p2 in rng f
then reconsider p29 = p2 as Element of PA2 ;
consider p1 being Element of PA1 such that
A7: p1 c= p29 by A1, Th105;
reconsider fp1 = f . p1 as Subset of A by TARSKI:def 3;
A8: p1 c= f . p1 by A4;
p29 meets f . p1

proof

ex x being Element of A st x in p1 by Th102;
hence p29 meets f . p1 by A7, A8, XBOOLE_0:3; :: thesis: verum

end;

then p29 = fp1 by EQREL_1:def 4;
hence p2 in rng f by A5, FUNCT_1:def 3; :: thesis: verum

end;

rng f c= PA2 by RELAT_1:def 19;
then rng f = PA2 by A6, XBOOLE_0:def 10;
then A9: f is one-to-one by A2, Th79;
A10: for x being Element of PA1 holds x = f . x

proof

let x be Element of PA1; :: thesis: x = f . x
reconsider fx = f . x as Subset of A by TARSKI:def 3;
consider E1 being Equivalence_Relation of A such that
A11: PA1 = Class E1 by EQREL_1:34;
assume x <> f . x ; :: thesis: contradiction
then consider a being set such that
A12: ( ( a in x & not a in f . x ) or ( a in f . x & not a in x ) ) by TARSKI:1;
A13: fx c= A ;
then A14: a in Class (E1,a) by A12, EQREL_1:20;
reconsider CE1a = Class (E1,a) as Element of PA1 by A13, A12, A11, EQREL_1:def 3;
reconsider fCE1a = f . CE1a as Subset of A by TARSKI:def 3;
A15: x c= f . x by A4;
CE1a c= f . CE1a by A4;
then fx meets fCE1a by A15, A12, A14, XBOOLE_0:3;
then fx = fCE1a by EQREL_1:def 4;
hence contradiction by A5, A9, A15, A12, A14, FUNCT_1:def 4; :: thesis: verum

end;

now

let x be set ; :: thesis: ( ( x in PA1 implies x in PA2 ) & ( x in PA2 implies x in PA1 ) )

hereby :: thesis: ( x in PA2 implies x in PA1 )

assume x in PA1 ; :: thesis: x in PA2
then reconsider x9 = x as Element of PA1 ;
set fx = f . x9;
f . x9 in PA2 ;
hence x in PA2 by A10; :: thesis: verum

end;

assume x in PA2 ; :: thesis: x in PA1
then consider y being set such that
A16: y in dom f and
A17: x = f . y by A6, FUNCT_1:def 3;
reconsider y9 = y as Element of PA1 by A16, FUNCT_2:def 1;
y9 = f . y9 by A10;
hence x in PA1 by A17; :: thesis: verum

end;

hence PA1 = PA2 by TARSKI:1; :: thesis: verum