theorem :: TREES_9:12

for t1, t2 being DecoratedTree st t1 is finite & Subtrees t1 = Subtrees t2 holds
t1 = t2