let X be set ; :: thesis: ( X is countable iff ex f being Function st
( dom f = NAT & X c= rng f ) )
thus ( X is countable implies ex f being Function st
( dom f = NAT & X c= rng f ) ) :: thesis: ( ex f being Function st
( dom f = NAT & X c= rng f ) implies X is countable )

proof

assume card X c= omega ; :: according to CARD_3:def 15 :: thesis: ex f being Function st
( dom f = NAT & X c= rng f )
hence ex f being Function st
( dom f = NAT & X c= rng f ) by CARD_1:28, CARD_1:84; :: thesis: verum

end;

assume ex f being Function st
( dom f = NAT & X c= rng f ) ; :: thesis: X is countable
hence card X c= omega by CARD_1:28, CARD_1:84; :: according to CARD_3:def 15 :: thesis: verum