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