theorem Th10: :: MATRIX13:10

for n being Nat holds card (2Set (Seg n)) = n choose 2