theorem Th8: :: TREES_4:8

for i being Nat
for j being Element of NAT st j < i holds
(elementary_tree i) | <*j*> = elementary_tree 0