let x be set ; :: thesis: ( <*x*> is DTree-yielding iff x is DecoratedTree )
( ( x is DecoratedTree implies {x} is constituted-DTrees ) & ( {x} is constituted-DTrees implies x is DecoratedTree ) & rng <*x*> = {x} ) by Th15, FINSEQ_1:56;
hence ( <*x*> is DTree-yielding iff x is DecoratedTree ) by Def11; :: thesis: verum