:: deftheorem defines -ImmediateSubtrees TREES_9:def 10 :
for t being finite DecoratedTree
for C being set
for b₃ being Function of (C -Subtrees t),((Subtrees t) *) holds
( b₃ = C -ImmediateSubtrees t iff for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = b₃ . d holds
d = (d . {}) -tree p );