set
e
= the
Element
of the
Sorts
of
(
FreeMSA
X
)
.
v
;
take
the
Element
of the
Sorts
of
(
FreeMSA
X
)
.
v
;
:: thesis:
the
Element
of the
Sorts
of
(
FreeMSA
X
)
.
v
is
finite
thus
the
Element
of the
Sorts
of
(
FreeMSA
X
)
.
v
is
finite
;
:: thesis:
verum