let X be set ; :: thesis: ( X is finite implies X is countable )
assume X is finite ; :: thesis: X is countable
then consider n being Nat such that
A1: X,n are_equipotent by CARD_1:74;
card n = card X by A1, CARD_1:21;
hence card X c= omega ; :: according to CARD_3:def 15 :: thesis: verum