theorem :: TREES_2:30

for T being finite-order Tree st ( for n being Nat ex C being finite Chain of T st card C = n ) holds
ex B being Chain of T st not B is finite