consider L being finite Chain ;
take L ; :: thesis: L is countable
the carrier of L is countable by CARD_4:43;
hence L is countable by Def2; :: thesis: verum