let A be non empty finite set ; 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; ( PA1 is_finer_than PA2 implies card PA2 <= card PA1 )
defpred S1[ object , object ] means ex A, B being set st
( A = $1 & B = $2 & A c= B );
assume A1:
PA1 is_finer_than PA2
; card PA2 <= card PA1
A2:
for e being object st e in PA1 holds
ex u being object st
( u in PA2 & S1[e,u] )
consider f being Function of PA1,PA2 such that
A3:
for e being object st e in PA1 holds
S1[e,f . e]
from FUNCT_2:sch 1(A2);
assume
card PA1 < card PA2
; 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;
S1[(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; verum