let A be non empty finite set ; :: thesis: for PA1, PA2 being a_partition of A st PA1 is_finer_than PA2 holds
card PA2 <= card PA1
let PA1, PA2 be a_partition of A; :: thesis: ( PA1 is_finer_than PA2 implies card PA2 <= card PA1 )
defpred S₁[ object , object ] means ex A, B being set st
( A = $1 & B = $2 & A c= B );
assume A1: PA1 is_finer_than PA2 ; :: thesis: card PA2 <= card PA1
A2: 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
A3: for e being object st e in PA1 holds
S₁[e,f . e] from FUNCT_2:sch 1(A2);
assume card PA1 < card PA2 ; :: thesis: contradiction
then card (Segm (card PA1)) in card (Segm (card PA2)) by NAT_1:41;
then consider p2i being object such that
A4: p2i in PA2 and
A5: for x being object st x in PA1 holds
f . x <> p2i by Th66;
reconsider p2i = p2i as Element of PA2 by A4;
consider q being Element of A such that
A6: q in p2i by Th85;
reconsider p2q = f . ((proj PA1) . q) as Element of PA2 ;
A7: ( p2q = p2i or p2q misses p2i ) by EQREL_1:def 4;
S₁[(proj PA1) . q,f . ((proj PA1) . q)] by A3;
then ( q in (proj PA1) . q & (proj PA1) . q c= p2q ) by EQREL_1:def 9;
hence contradiction by A5, A6, A7, XBOOLE_0:3; :: thesis: verum