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