let X, Y be set ; :: thesis: ( X,Y are_equipotent & X is countable implies Y is countable )

assume ( X,Y are_equipotent & card X c= omega ) ; :: according to CARD_3:def 14 :: thesis: Y is countable

hence card Y c= omega by CARD_1:5; :: according to CARD_3:def 14 :: thesis: verum

assume ( X,Y are_equipotent & card X c= omega ) ; :: according to CARD_3:def 14 :: thesis: Y is countable

hence card Y c= omega by CARD_1:5; :: according to CARD_3:def 14 :: thesis: verum