:: deftheorem defines succ TREES_2:def 5 :
for W being Tree
for w being Element of W holds succ w = { (w ^ <*n*>) where n is Nat : w ^ <*n*> in W } ;