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