let T be finite-branching Tree; :: thesis: ( T is finite iff ex n being Element of NAT st T -level n = {} )

now

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

now

assume A2: for n being Element of NAT holds not T -level n = {} ; :: thesis: contradiction
A3: for n being Element of NAT ex C being finite Chain of T st card C = n

proof

let n be Element of NAT ; :: thesis: ex C being finite Chain of T st card C = n
T -level n <> {} by A2;
then consider t being set such that
A4: t in T -level n by XBOOLE_0:def 1;
consider w being Element of T such that
A5: ( t = w & len w = n ) by A4;
ProperPrefixes w is finite Chain of T by Th16;
then consider C being finite Chain of T such that
A6: C = ProperPrefixes w ;
card C = n by A5, A6, TREES_1:68;
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:31;
hence contradiction by A1; :: thesis: verum

end;

hence ex n being Element of NAT st T -level n = {} ; :: thesis: verum

end;

hence ( T is finite implies ex n being Element of NAT st T -level n = {} ) ; :: thesis: ( ex n being Element of NAT st T -level n = {} implies T is finite )
given n being Element of NAT such that A7: T -level n = {} ; :: thesis: T is finite
deffunc H₁( Element of NAT ) -> Level of T = T -level $1;
set X = { H₁(m) where m is Element of NAT : m <= n } ;
A8: T c= union { H₁(m) where m is Element of NAT : m <= n }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T or x in union { H₁(m) where m is Element of NAT : m <= n } )
assume x in T ; :: thesis: x in union { H₁(m) where m is Element of NAT : m <= n }
then reconsider t = x as Element of T ;
A9: len t < n

proof

assume A10: n <= len t ; :: thesis: contradiction
consider q being FinSequence such that
A11: ( q = t | (Seg n) & q is_a_prefix_of t ) by Th4;
A12: ( len q = n & q is_a_prefix_of t ) by A10, A11, FINSEQ_1:21;
reconsider q = q as Element of T by A11, TREES_1:45;
q in T -level n by A12;
hence contradiction by A7; :: thesis: verum

end;

consider m being Element of NAT such that
A13: m = len t ;
A14: H₁(m) in { H₁(m) where m is Element of NAT : m <= n } by A9, A13;
t in H₁(m) by A13;
hence x in union { H₁(m) where m is Element of NAT : m <= n } by A14, TARSKI:def 4; :: thesis: verum

end;

A15: { H₁(m) where m is Element of NAT : m <= n } is finite

proof

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

proof

let k be Nat; :: thesis: ( k in Seg (n + 1) implies ex x being set st S₁[k,x] )
assume k in Seg (n + 1) ; :: thesis: ex x being set st S₁[k,x]
then 0 <> k by FINSEQ_1:3;
then consider l being Nat such that
A18: k = l + 1 by NAT_1:6;
reconsider l = l as Element of NAT by ORDINAL1:def 13;
consider x being set such that
A19: x = H₁(l) ;
take x ; :: thesis: S₁[k,x]
take l ; :: thesis: ex m being Element of 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 A18, A19; :: thesis: verum

end;

consider p being FinSequence such that
A20: ( 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(A17);
A21: ( dom p = Seg (n + 1) & ( for k being Element of NAT st k + 1 in Seg (n + 1) holds
p . (k + 1) = H₁(k) ) )

proof

thus dom p = Seg (n + 1) by A20; :: thesis: for k being Element of NAT st k + 1 in Seg (n + 1) holds
p . (k + 1) = H₁(k)
thus for k being Element of NAT st k + 1 in Seg (n + 1) holds
p . (k + 1) = H₁(k) :: thesis: verum

proof

let k be Element of 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 Element of NAT st
( m = l + 1 & k + 1 = m & H₁(l) = p . (k + 1) ) by A20;
hence p . (k + 1) = H₁(k) ; :: thesis: verum

end;

end;

rng p = { H₁(m) where m is Element of NAT : m <= n }

proof

thus rng p c= { H₁(m) where m is Element of NAT : m <= n } :: according to XBOOLE_0:def 10 :: thesis: { H₁(m) where m is Element of NAT : m <= n } c= rng p

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in { H₁(m) where m is Element of NAT : m <= n } )
assume y in rng p ; :: thesis: y in { H₁(m) where m is Element of NAT : m <= n }
then consider x being set such that
A22: ( x in dom p & p . x = y ) by FUNCT_1:def 5;
dom p = { k where k is Element of NAT : ( 1 <= k & k <= n + 1 ) } by A21, FINSEQ_1:def 1;
then consider k being Element of NAT such that
A23: ( x = k & 1 <= k & k <= n + 1 ) by A22;
0 + 1 <= k by A23;
then 0 < k by NAT_1:13;
then consider m being Nat such that
A24: m + 1 = k by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
m + 1 in Seg (n + 1) by A23, A24, FINSEQ_1:3;
then A25: p . (m + 1) = H₁(m) by A21;
m <= n by A23, A24, XREAL_1:8;
hence y in { H₁(m) where m is Element of NAT : m <= n } by A22, A23, A24, A25; :: thesis: verum

end;

thus { H₁(m) where m is Element of NAT : m <= n } c= rng p :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { H₁(m) where m is Element of NAT : m <= n } or y in rng p )
assume y in { H₁(m) where m is Element of NAT : m <= n } ; :: thesis: y in rng p
then consider m being Element of NAT such that
A26: ( y = H₁(m) & m <= n ) ;
0 <= m by NAT_1:2;
then 0 + 1 <= m + 1 by XREAL_1:8;
then ( 1 <= m + 1 & m + 1 <= n + 1 ) by A26, XREAL_1:8;
then A27: m + 1 in Seg (n + 1) by FINSEQ_1:3;
then p . (m + 1) = H₁(m) by A21;
hence y in rng p by A21, A26, A27, FUNCT_1:def 5; :: thesis: verum

end;

end;

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

end;

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

proof

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

end;

then union { H₁(m) where m is Element of NAT : m <= n } is finite by A15, FINSET_1:25;
hence T is finite by A8; :: thesis: verum