theorem Th90: :: CARD_3:93

for X being set holds
( X is countable iff ex f being Function st
( dom f = omega & X c= rng f ) ) by CARD_1:12, CARD_1:47;