for W being Tree
for w being Element of W st W is finite-order holds
succ w is finite