:: deftheorem Def5 defines succ TREES_9:def 5 :
for t being finite-branching Tree
for p being Element of t
for b₃ being one-to-one FinSequence of t holds
( b₃ = p succ iff ( len b₃ = card (succ p) & rng b₃ = succ p & ( for i being Nat st i < len b₃ holds
b₃ . (i + 1) = p ^ <*i*> ) ) );