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 x in succ w ; :: thesis: x in { (w ^ <*(r - 1)*>) where r is Real : r in Seg n }
then consider k being Element of NAT such that
A5: ( x = w ^ <*k*> & w ^ <*k*> in W ) ;
not w ^ <*n*> in W by A1;
then ( k < n & k + 1 = 1 + k ) by A5, TREES_1:def 5;
then ( k + 1 <= n & 1 <= k + 1 ) by NAT_1:11, NAT_1:13;
then ( k + 1 in Seg n & (k + 1) - 1 = k ) by FINSEQ_1:3;
hence x in { (w ^ <*(r - 1)*>) where r is Real : r in Seg n } by A5; :: 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 = { H₁(r) where r is Real : r in Seg n } ;
{ H₁(r) where r is Real : r in Seg n } is finite from FRAENKEL:sch 21(A2);
then reconsider C = { H₁(r) where r is Real : r in Seg n } as finite set ;
A6: C = { H₁(r) where r is Real : r in Seg n } ;
card C <= card (Seg n) from TREES_2:sch 3(A6);
then ( card C <= n & card B <= card C ) by A4, FINSEQ_1:78, NAT_1:44;
hence card B <= n by XXREAL_0:2; :: thesis: verum