let T be 1-sorted ; :: thesis: ( T is finite implies T is countable )
assume T is finite ; :: thesis: T is countable
then the carrier of T is countable by CARD_4:1;
hence T is countable by ORDERS_4:def 2; :: thesis: verum