theorem Th16: :: CARD_FIN:17

for X, Y being finite set
for x, y being object st x <> y holds
(Y --> y) +* (X --> x) in Choose ((X \/ Y),(card X),x,y)