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