let W be Tree; :: thesis: ( W is finite-order implies ex n being Element of NAT st
for w being Element of W ex B being finite set st
( B = succ w & card B <= n ) )
given n being Element of 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 Element of 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 H₁( Real) -> set = w ^ <*($1 - 1)*>;
A3: { H₁(r) where r is Real : r in Seg n } is finite from FRAENKEL:sch 21(A2);
A4: succ w c= { (w ^ <*(r - 1)*>) where r is Real : r in Seg n }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in succ w or x in { (w ^ <*(r - 1)*>) where r is Real : r in Seg n } )
assume A5: x in succ w ; :: thesis: x in { (w ^ <*(r - 1)*>) where r is Real : r in Seg n }
consider k being Element of NAT such that
A6: x = w ^ <*k*> and
A7: w ^ <*k*> in W by A5;
A8: not w ^ <*n*> in W by A1;
A9: k < n by A7, A8, TREES_1:def 5;
A10: k + 1 <= n by A9, NAT_1:13;
A11: 1 <= k + 1 by NAT_1:11;
A12: k + 1 in Seg n by A10, A11, FINSEQ_1:3;
A13: (k + 1) - 1 = k ;
thus x in { (w ^ <*(r - 1)*>) where r is Real : r in Seg n } by A6, A12, A13; :: thesis: verum

end;

reconsider B = succ w as finite set by A3, A4;
take B ; :: thesis: ( B = succ w & card B <= n )
thus B = succ w ; :: thesis: card B <= n
set C = { H₁(r) where r is Real : r in Seg n } ;
A14: { H₁(r) where r is Real : r in Seg n } is finite from FRAENKEL:sch 21(A2);
reconsider C = { H₁(r) where r is Real : r in Seg n } as finite set by A14;
A15: C = { H₁(r) where r is Real : r in Seg n } ;
A16: card C <= card (Seg n) from TREES_2:sch 3(A15);
A17: card C <= n by A16, FINSEQ_1:78;
A18: card B <= card C by A4, NAT_1:44;
thus card B <= n by A17, A18, XXREAL_0:2; :: thesis: verum