let T be 1-sorted ; :: thesis: ( T is countable iff card ([#] T) c= omega )

hereby :: thesis: ( card ([#] T) c= omega implies T is countable )

assume T is countable ; :: thesis: card ([#] T) c= omega
then [#] T is countable by ORDERS_4:def 2;
hence card ([#] T) c= omega by CARD_3:def 14; :: thesis: verum

end;

assume card ([#] T) c= omega ; :: thesis: T is countable
then [#] T is countable by CARD_3:def 14;
hence T is countable by ORDERS_4:def 2; :: thesis: verum