:: deftheorem Def8 defines countable SUPINF_2:def 8 :
for D being non empty set
for IT being Subset of D holds
( IT is countable iff ( IT is empty or ex F being sequence of D st IT = rng F ) );