Description: A set equinumerous to a finite set is finite. (Contributed by Mario Carneiro, 12-Mar-2015)