theorem Th43: :: TREES_9:43

for T being Tree
for t being Element of T holds ProperPrefixes t is finite Chain of T