theorem :: TREES_2:12

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 ) ;