theorem Th9: :: CIRCTRM1:9

for X1, X2 being non empty constituted-DTrees set st ( for t being Element of X1 holds t is finite ) & ( for t being Element of X2 holds t is finite ) holds
for C being set holds C -ImmediateSubtrees (X1 \/ X2) = (C -ImmediateSubtrees X1) +* (C -ImmediateSubtrees X2)