theorem Th17: :: CARD_FIN:18

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