theorem :: TREES_4:22

for x being object
for T being DecoratedTree holds x -tree <*T*> = ((elementary_tree 1) --> x) with-replacement (<*0*>,T)