reconsider T = T as Element of Trees D by TREES_3:def 7;
reconsider t = <*T*> as Element of (Trees D) * by FINSEQ_1:def 11;
A1: d -tree T = d -tree t ;
thus d -tree T is DecoratedTree of D by A1; :: thesis: verum