let T be finite-order Tree; :: thesis: ( ( for n being Nat ex C being finite Chain of T st card C = n ) implies ex B being Chain of T st not B is finite )
for t being Element of T holds succ t is finite ;
hence ( ( for n being Nat ex C being finite Chain of T st card C = n ) implies ex B being Chain of T st not B is finite ) by Th29; :: thesis: verum