let X be set ; :: thesis: ( X is finite implies X is countable )
assume X is finite ; :: thesis: X is countable
then consider n being natural number such that
A1: X,n are_equipotent by CARD_1:43;
card n = card X by A1, CARD_1:5;
hence card X c= omega ; :: according to CARD_3:def 14 :: thesis: verum