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 )
assume A1: PA1 is_finer_than PA2 ; :: thesis: card PA2 <= card PA1
assume card PA1 < card PA2 ; :: thesis: contradiction
then A2: card (card PA1) in card (card PA2) by NAT_1:42;
defpred S₁[ set , set ] means $1 c= $2;
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);
consider p2i being set such that
A5: p2i in PA2 and
A6: for x being set st x in PA1 holds
f . x <> p2i by A2, FINSEQ_4:81;
reconsider p2i = p2i as Element of PA2 by A5;
consider q being Element of A such that
A7: q in p2i by Th11;
reconsider p2q = f . ((proj PA1) . q) as Element of PA2 ;
A8: q in (proj PA1) . q by BORSUK_1:def 1;
A9: (proj PA1) . q c= p2q by A4;
( p2q = p2i or p2q misses p2i ) by EQREL_1:def 6;
hence contradiction by A6, A7, A8, A9, XBOOLE_0:3; :: thesis: verum