let
t
be
Element
of
FinTrees
D
;
:: thesis:
t
is
finite
dom
t
is
finite
;
hence
t
is
finite
by
FINSET_1:10
;
:: thesis:
verum