let X be set ; :: thesis: ( X is denumerable implies ( X is countable & not X is finite ) )
assume A1: card X = omega ; :: according to CARD_3:def 15 :: thesis: ( X is countable & not X is finite )
hence card X c= omega ; :: according to CARD_3:def 14 :: thesis: not X is finite
thus not X is finite by A1; :: thesis: verum