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

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