let X be set ; :: thesis: ( X is countable & X is infinite implies X is denumerable )
assume A2: 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 Th85;
hence card X = omega by A2, XBOOLE_0:def 10; :: according to CARD_3:def 15 :: thesis: verum