:: deftheorem Def14 defines countable CARD_3:def 14 :
for X being set holds
( X is countable iff card X c= omega );