set L = the finite Chain ;
take the finite Chain ; :: thesis: the finite Chain is countable
the carrier of the finite Chain is countable by CARD_4:1;
hence the finite Chain is countable ; :: thesis: verum