for T being Tree
for B being Branch of T
for t being Element of T st t in B & not B is finite holds
ex t9 being Element of T st
( t9 in B & t9 in succ t )