consider T being DecoratedTree of ;
set X = {T};
{T} is constituted-DTrees

proof

let x be set ; :: according to TREES_3:def 5 :: thesis: ( x in {T} implies x is DecoratedTree )
assume x in {T} ; :: thesis: x is DecoratedTree
hence x is DecoratedTree by TARSKI:def 1; :: thesis: verum

end;

then reconsider X = {T} as constituted-DTrees set ;
X is DTree-set of D

proof

let x be set ; :: according to TREES_3:def 6 :: thesis: ( x in X implies x is DecoratedTree of )
assume x in X ; :: thesis: x is DecoratedTree of
hence x is DecoratedTree of by TARSKI:def 1; :: thesis: verum

end;

then reconsider X = X as DTree-set of D ;
take X ; :: thesis: ( X is finite & not X is empty )
thus X is finite ; :: thesis: not X is empty
thus not X is empty ; :: thesis: verum