let T be finite-order Tree; :: thesis: ( ( for n being Element of 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 Element of 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 Th31; :: thesis: verum