for T being Tree st ( for n being Nat ex C being finite Chain of T st card C = n ) & ( for t being Element of T holds succ t is finite ) holds
ex B being Chain of T st not B is finite