theorem :: TREES_1:30

for n being Nat
for p being FinSequence of NAT holds
( not p in elementary_tree n or p = {} or ex k being Nat st
( k < n & p = <*k*> ) )