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