theorem Th27: :: TREES_1:28

for k, n being Nat st k < n holds
<*k*> in elementary_tree n