let T be finite-branching Tree; :: thesis: ( T is finite iff ex n being Nat st T -level n = {} )
deffunc H₁( Nat) -> Level of T = T -level $1;

now :: thesis: ( T is finite implies ex n being Nat st T -level n = {} )

assume A1: T is finite ; :: thesis: ex n being Nat st T -level n = {}

now :: thesis: ex n being Nat st T -level n = {}

assume A2: for n being Nat holds not T -level n = {} ; :: thesis: contradiction
A3: 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 A2;
then consider t being object such that
A4: t in T -level n by XBOOLE_0:def 1;
consider w being Element of T such that
t = w and
A5: len w = n by A4;
ProperPrefixes w is finite Chain of T by Th43;
then consider C being finite Chain of T such that
A6: C = ProperPrefixes w ;
card C = n by A5, A6, 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 ;
then not for C being Chain of T holds C is finite by A3, TREES_2:29;
hence contradiction by A1; :: thesis: verum

end;

hence ex n being Nat st T -level n = {} ; :: thesis: verum

end;

hence ( T is finite implies ex n being Nat st T -level n = {} ) ; :: thesis: ( ex n being Nat st T -level n = {} implies T is finite )
given n being Nat such that A7: T -level n = {} ; :: thesis: T is finite
set X = { H₁(m) where m is Nat : m <= n } ;
A8: T c= union { H₁(m) where m is Nat : m <= n }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in T or x in union { H₁(m) where m is Nat : m <= n } )
assume x in T ; :: thesis: x in union { H₁(m) where m is Nat : m <= n }
then reconsider t = x as Element of T ;
consider m being Nat such that
A9: m = len t ;
A10: t in H₁(m) by A9;
len t < n

proof

consider q being FinSequence such that
A11: q = t | (Seg n) and
A12: q is_a_prefix_of t by Th32;
assume n <= len t ; :: thesis: contradiction
then A13: len q = n by A11, FINSEQ_1:17;
reconsider q = q as Element of T by A12, TREES_1:20;
q in T -level n by A13;
hence contradiction by A7; :: thesis: verum

end;

then H₁(m) in { H₁(m) where m is Nat : m <= n } by A9;
hence x in union { H₁(m) where m is Nat : m <= n } by A10, TARSKI:def 4; :: thesis: verum

end;

A14: { H₁(m) where m is Nat : m <= n } is finite

proof

defpred S₁[ set , object ] means ex l, m being Nat st
( m = l + 1 & $1 = m & H₁(l) = $2 );
A15: for k being Nat st k in Seg (n + 1) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (n + 1) implies ex x being object st S₁[k,x] )
assume k in Seg (n + 1) ; :: thesis: ex x being object st S₁[k,x]
then 0 <> k by FINSEQ_1:1;
then consider l being Nat such that
A16: k = l + 1 by NAT_1:6;
reconsider l = l as Nat ;
consider x being set such that
A17: x = H₁(l) ;
take x ; :: thesis: S₁[k,x]
take l ; :: thesis: ex m being Nat st
( m = l + 1 & k = m & H₁(l) = x )
take l + 1 ; :: thesis: ( l + 1 = l + 1 & k = l + 1 & H₁(l) = x )
thus ( l + 1 = l + 1 & k = l + 1 & H₁(l) = x ) by A16, A17; :: thesis: verum

end;

consider p being FinSequence such that
A18: ( dom p = Seg (n + 1) & ( for k being Nat st k in Seg (n + 1) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A15);
A19: for k being Nat st k + 1 in Seg (n + 1) holds
p . (k + 1) = H₁(k)

proof

let k be Nat; :: thesis: ( k + 1 in Seg (n + 1) implies p . (k + 1) = H₁(k) )
assume k + 1 in Seg (n + 1) ; :: thesis: p . (k + 1) = H₁(k)
then ex l, m being Nat st
( m = l + 1 & k + 1 = m & H₁(l) = p . (k + 1) ) by A18;
hence p . (k + 1) = H₁(k) ; :: thesis: verum

end;

{ H₁(m) where m is Nat : m <= n } c= rng p

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { H₁(m) where m is Nat : m <= n } or y in rng p )
assume y in { H₁(m) where m is Nat : m <= n } ; :: thesis: y in rng p
then consider m being Nat such that
A20: y = H₁(m) and
A21: m <= n ;
A22: 0 + 1 <= m + 1 by XREAL_1:6;
m + 1 <= n + 1 by A21, XREAL_1:6;
then A23: m + 1 in Seg (n + 1) by A22, FINSEQ_1:1;
then p . (m + 1) = H₁(m) by A19;
hence y in rng p by A18, A20, A23, FUNCT_1:def 3; :: thesis: verum

end;

hence { H₁(m) where m is Nat : m <= n } is finite ; :: thesis: verum

end;

for Y being set st Y in { H₁(m) where m is Nat : m <= n } holds
Y is finite

proof

let Y be set ; :: thesis: ( Y in { H₁(m) where m is Nat : m <= n } implies Y is finite )
assume Y in { H₁(m) where m is Nat : m <= n } ; :: thesis: Y is finite
then ex m being Nat st
( Y = H₁(m) & m <= n ) ;
hence Y is finite by Th46; :: thesis: verum

end;

then union { H₁(m) where m is Nat : m <= n } is finite by A14, FINSET_1:7;
hence T is finite by A8; :: thesis: verum