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