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