let X be non empty finite set ; :: thesis: for PX being a_partition of X holds card PX <= card X
let PX be a_partition of X; :: thesis: card PX <= card X
assume card PX > card X ; :: thesis: contradiction
then card (Segm (card X)) in card (Segm (card PX)) by NAT_1:41;
then consider Pi being object such that
A1: Pi in PX and
A2: for x being object st x in X holds
(proj PX) . x <> Pi by Th66;
reconsider Pi = Pi as Element of PX by A1;
consider q being Element of X such that
A3: q in Pi by Th85;
reconsider Pq = (proj PX) . q as Element of PX ;
A4: ( Pq = Pi or Pq misses Pi ) by EQREL_1:def 4;
q in Pq by EQREL_1:def 9;
hence contradiction by A2, A3, A4, XBOOLE_0:3; :: thesis: verum