let T be finite-branching Tree; :: thesis: ( not T is finite implies ex C being Chain of T st not C is finite )
assume A1: not T is finite ; :: thesis: not for C being Chain of T holds C is finite
A2: for n being Nat ex C being finite Chain of T st card C = n
proof
let n be Nat; :: thesis: ex C being finite Chain of T st card C = n
T -level n <> {} by A1, Th47;
then consider t being object such that
A3: t in T -level n by XBOOLE_0:def 1;
A4: ex w being Element of T st
( t = w & len w = n ) by A3;
reconsider t = t as Element of T by A3;
ProperPrefixes t is finite Chain of T by Th43;
then consider C being finite Chain of T such that
A5: C = ProperPrefixes t ;
card C = n by A4, A5, TREES_1:35;
hence ex C being finite Chain of T st card C = n ; :: thesis: verum
end;
for t being Element of T holds succ t is finite ;
hence not for C being Chain of T holds C is finite by A2, TREES_2:29; :: thesis: verum