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₁[ object , object ] means ex A, B being set st
( A = $1 & B = $2 & A c= B );
assume that
A1: PA1 is_finer_than PA2 and
A2: card PA1 = card PA2 ; :: thesis: PA1 = PA2
A3: for e being object st e in PA1 holds
ex u being object st
( u in PA2 & S₁[e,u] )

proof

let e be object ; :: thesis: ( e in PA1 implies ex u being object st
( u in PA2 & S₁[e,u] ) )
reconsider ee = e as set by TARSKI:1;
assume e in PA1 ; :: thesis: ex u being object st
( u in PA2 & S₁[e,u] )
then ee in PA1 ;
then ex u being set st
( u in PA2 & ee c= u ) by SETFAM_1:def 2, A1;
hence ex u being object st
( u in PA2 & S₁[e,u] ) ; :: thesis: verum

end;

consider f being Function of PA1,PA2 such that
A4: for e being object 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 object ; :: 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, Th88;
reconsider fp1 = f . p1 as Subset of A by TARSKI:def 3;
S₁[p1,f . p1] by A4;
then A8: p1 c= f . p1 ;
p29 meets f . p1

proof

ex x being Element of A st x in p1 by Th85;
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;
then f is onto by FUNCT_2:def 3;
then A9: f is one-to-one by A2, Lm1;
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 object such that
A12: ( ( a in x & not a in f . x ) or ( a in f . x & not a in x ) ) by TARSKI:2;
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;
S₁[x,f . x] by A4;
then A15: x c= f . x ;
S₁[CE1a,f . CE1a] by A4;
then CE1a c= f . CE1a ;
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; :: thesis: verum

end;

now :: thesis: for x being object holds
( ( x in PA1 implies x in PA2 ) & ( x in PA2 implies x in PA1 ) )

let x be object ; :: 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 object 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:2; :: thesis: verum