theorem Th18: :: TREES_2:18

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