for T being 1-sorted holds
( T is countable iff card ([#] T) c= omega ) by CARD_3:def 14, ORDERS_4:def 2;