theorem Th2: :: TREES_9:2

for t being Tree
for p, q being FinSequence of NAT st p ^ q in t holds
t | (p ^ q) = (t | p) | q