theorem Th50: :: TREES_9:50

for T being Tree
for C being Chain of T
for t being Element of T st t in C & not C is finite holds
ex t9 being Element of T st
( t9 in C & t is_a_proper_prefix_of t9 )