theorem :: BINTREE1:1

for D being non empty set
for t being DecoratedTree of D holds roots <*t*> = <*(root-label t)*> by DTCONSTR:4;