let W be Tree; :: thesis: ( W is finite-order implies ex n being Nat st
for w being Element of W ex B being finite set st
( B = succ w & card B <= n ) )
given n being Nat such that A1: for w being Element of W holds not w ^ <*n*> in W ; :: according to TREES_2:def 2 :: thesis: ex n being Nat st
for w being Element of W ex B being finite set st
( B = succ w & card B <= n )
A2: Seg n is finite ;
take n ; :: thesis: for w being Element of W ex B being finite set st
( B = succ w & card B <= n )
let w be Element of W; :: thesis: ex B being finite set st
( B = succ w & card B <= n )
deffunc H1( Real) -> set = w ^ <*($1 - 1)*>;
A3: { H1(r) where r is Element of REAL : r in Seg n } is finite from FRAENKEL:sch 21(A2);
 A4: succ w c= { (w ^ <*(r - 1)*>) where r is Element of REAL : r in Seg n }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in succ w or x in { (w ^ <*(r - 1)*>) where r is Element of REAL : r in Seg n } )
assume x in succ w ; :: thesis: x in { (w ^ <*(r - 1)*>) where r is Element of REAL : r in Seg n }
then consider k being Nat such that
A5: x = w ^ <*k*> and
A6: w ^ <*k*> in W ;
not w ^ <*n*> in W by A1;
then k < n by A6, TREES_1:def 3;
then A7: k + 1 <= n by NAT_1:13;
1 <= k + 1 by NAT_1:11;
then A8: k + 1 in Seg n by A7, FINSEQ_1:1;
A9: k + 1 in REAL by XREAL_0:def 1;
(k + 1) - 1 = k ;
hence x in { (w ^ <*(r - 1)*>) where r is Element of REAL : r in Seg n } by A5, A8, A9; :: thesis: verum
end;
then reconsider B = succ w as finite set by A3;
take B ; :: thesis: ( B = succ w & card B <= n )
thus B = succ w ; :: thesis: card B <= n
set C = { H1(r) where r is Element of REAL : r in Seg n } ;
{ H1(r) where r is Element of REAL : r in Seg n } is finite from FRAENKEL:sch 21(A2);
 then reconsider C = { H1(r) where r is Element of REAL : r in Seg n } as finite set ;
A10: C = { H1(r) where r is Element of REAL : r in Seg n } ;
card C <= card (Seg n) from TREES_2:sch 3(A10);
 then A11: card C <= n by FINSEQ_1:57;
card B <= card C by A4, NAT_1:43;
hence card B <= n by A11, XXREAL_0:2; :: thesis: verum