theorem Th8: :: MYCIELSK:8

for X being set
for P being finite a_partition of X
for S being Subset of X holds card (P | S) <= card P