for X being finite set
for n being Nat holds card { Y where Y is Subset of X : card Y = n } = (card X) choose n