theorem Th11: :: CARD_FIN:12
for X being finite set
for x1, x2 being object holds card (Choose (X,(card X),x1,x2)) = 1