let T be finite-branching Tree; :: thesis: for n being Element of NAT holds T -level n is finite
defpred S₁[ Element of NAT ] means T -level $1 is finite;
A1: S₁[ 0 ] by Th17;
A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: T -level n is finite ; :: thesis: S₁[n + 1]
A4: T -level (n + 1) = union { (succ w) where w is Element of T : len w = n } by Th18;
set X = { (succ w) where w is Element of T : len w = n } ;
A5: { (succ w) where w is Element of T : len w = n } is finite

proof

defpred S₂[ set , set ] means ex w being Element of T st
( $1 = w & $2 = succ w );
A6: for x being set st x in T -level n holds
ex y being set st S₂[x,y]

proof

let x be set ; :: thesis: ( x in T -level n implies ex y being set st S₂[x,y] )
assume x in T -level n ; :: thesis: ex y being set st S₂[x,y]
then consider w being Element of T such that
A7: w = x ;
consider y being set such that
A8: y = succ w ;
take y ; :: thesis: S₂[x,y]
take w ; :: thesis: ( x = w & y = succ w )
thus ( x = w & y = succ w ) by A7, A8; :: thesis: verum

end;

consider f being Function such that
A9: ( dom f = T -level n & ( for x being set st x in T -level n holds
S₂[x,f . x] ) ) from CLASSES1:sch 1(A6);
A10: { (succ w) where w is Element of T : len w = n } c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (succ w) where w is Element of T : len w = n } or x in rng f )
assume x in { (succ w) where w is Element of T : len w = n } ; :: thesis: x in rng f
then consider w being Element of T such that
A11: ( x = succ w & len w = n ) ;
A12: w in T -level n by A11;
then consider w' being Element of T such that
A13: ( w = w' & f . w = succ w' ) by A9;
thus x in rng f by A9, A11, A12, A13, FUNCT_1:def 5; :: thesis: verum

end;

card (rng f) c= card (dom f) by CARD_1:28;
then rng f is finite by A3, A9;
hence { (succ w) where w is Element of T : len w = n } is finite by A10; :: thesis: verum

end;

for Y being set st Y in { (succ w) where w is Element of T : len w = n } holds
Y is finite

proof

let Y be set ; :: thesis: ( Y in { (succ w) where w is Element of T : len w = n } implies Y is finite )
assume Y in { (succ w) where w is Element of T : len w = n } ; :: thesis: Y is finite
then consider w being Element of T such that
A14: ( Y = succ w & len w = n ) ;
thus Y is finite by A14; :: thesis: verum

end;

hence T -level (n + 1) is finite by A4, A5, FINSET_1:25; :: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2); :: thesis: verum