theorem :: BINTREE1:2

for D being non empty set
for t1, t2 being DecoratedTree of D holds roots <*t1,t2*> = <*(root-label t1),(root-label t2)*> by DTCONSTR:6;