let
n
be
Nat
;
:: thesis:
square-downarrow
n
is
finite
Subset
of
[:
NAT
,
NAT
:]
[:
(
Segm
n
)
,
(
Segm
n
)
:]
is
finite
;
hence
square-downarrow
n
is
finite
Subset
of
[:
NAT
,
NAT
:]
by
Th30
;
:: thesis:
verum