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