let X be set ; :: thesis: ( X is countable & not X is finite implies X is denumerable )
assume A2: card X c= omega ; :: according to CARD_3:def 14 :: thesis: ( X is finite or X is denumerable )
assume not X is finite ; :: thesis: X is denumerable
then omega c= card X by Th102;
hence card X = omega by A2, XBOOLE_0:def 10; :: according to CARD_3:def 15 :: thesis: verum