set X = { the DecoratedTree of D};
{ the DecoratedTree of D} is constituted-DTrees by TARSKI:def 1;
then reconsider X = { the DecoratedTree of D} as non empty constituted-DTrees set ;
X is DTree-set of D

proof

let x be object ; :: according to TREES_3:def 6 :: thesis: ( x in X implies x is DecoratedTree of D )
thus ( x in X implies x is DecoratedTree of D ) 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 & not X is empty ) ; :: thesis: verum