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