:: deftheorem defines denumerable CARD_3:def 15 :
for X being set holds
( X is denumerable iff card X = omega );