theorem Th7: :: MYCIELSK:7

for X being set
for P being a_partition of X holds card P c= card X