:: deftheorem defines roots TREES_3:def 18 :
for p being FinSequence st p is DTree-yielding holds
for b₂ being FinSequence holds
( b₂ = roots p iff ( dom b₂ = dom p & ( for i being Element of NAT st i in dom p holds
ex T being DecoratedTree st
( T = p . i & b₂ . i = T . {} ) ) ) );