theorem :: GLIBPRE0:20

for X being finite set holds card (2Set X) = (card X) choose 2