for W being Tree
for w being Element of W
for n being Nat holds
( w ^ <*n*> in succ w iff w ^ <*n*> in W ) ;