set IT = elementary_tree n;
elementary_tree n, Seg (n + 1) are_equipotent

proof

defpred S₁[ object , object ] means ( ( n = {} & c₂ = 1 ) or ex n being Nat st
( n = <*n*> & c₂ = n + 2 ) );
A1: for x, y, z being set st x in elementary_tree n & S₁[x,y] & S₁[x,z] holds
y = z

proof

let x, y, z be set ; :: thesis: ( x in elementary_tree n & S₁[x,y] & S₁[x,z] implies y = z )
assume that
x in elementary_tree n and
A2: ( ( ( x = {} & y = 1 ) or ex n being Nat st
( x = <*n*> & y = n + 2 ) ) & ( ( x = {} & z = 1 ) or ex n being Nat st
( x = <*n*> & z = n + 2 ) ) ) ; :: thesis: y = z

now :: thesis: ( ex n1 being Nat st
( x = <*n1*> & y = n1 + 2 ) & ex n2 being Nat st
( x = <*n2*> & z = n2 + 2 ) implies y = z )

given n1 being Nat such that A3: ( x = <*n1*> & y = n1 + 2 ) ; :: thesis: ( ex n2 being Nat st
( x = <*n2*> & z = n2 + 2 ) implies y = z )
given n2 being Nat such that A4: ( x = <*n2*> & z = n2 + 2 ) ; :: thesis: y = z
<*n1*> . 1 = n1 ;
hence y = z by A3, A4, FINSEQ_1:def 8; :: thesis: verum

end;

hence y = z by A2; :: thesis: verum

end;

A5: for x being object st x in elementary_tree n holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in elementary_tree n implies ex y being object st S₁[x,y] )
assume A6: x in elementary_tree n ; :: thesis: ex y being object st S₁[x,y]

A7: now :: thesis: ( x in { <*k*> where k is Nat : k < n } implies ex y being set st S₁[x,y] )

assume x in { <*k*> where k is Nat : k < n } ; :: thesis: ex y being set st S₁[x,y]
then consider k being Nat such that
A8: x = <*k*> and
k < n ;
reconsider y = k + 2 as set ;
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] by A8; :: thesis: verum

end;

now :: thesis: ( x in {{}} implies ex y being set st S₁[x,y] )

assume A9: x in {{}} ; :: thesis: ex y being set st S₁[x,y]
reconsider y = 1 as set ;
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] by A9, TARSKI:def 1; :: thesis: verum

end;

hence ex y being object st S₁[x,y] by A6, A7, XBOOLE_0:def 3; :: thesis: verum

end;

consider f being Function such that
A10: ( dom f = elementary_tree n & ( for x being object st x in elementary_tree n holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A5);
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & dom f = elementary_tree n & rng f = Seg (n + 1) )
thus f is one-to-one :: thesis: ( dom f = elementary_tree n & rng f = Seg (n + 1) )

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A11: x in dom f and
A12: y in dom f and
A13: f . x = f . y ; :: thesis: x = y
A14: ( ( x = {} & f . x = 1 ) or ex n being Nat st
( x = <*n*> & f . x = n + 2 ) ) by A10, A11;
A15: ( ( y = {} & f . y = 1 ) or ex n being Nat st
( y = <*n*> & f . y = n + 2 ) ) by A10, A12;

A16: now :: thesis: ( x = {} & f . x = 1 implies for n being Nat holds
( not y = <*n*> or not f . y = n + 2 ) )

assume that
x = {} and
A17: f . x = 1 ; :: thesis: for n being Nat holds
( not y = <*n*> or not f . y = n + 2 )
given n being Nat such that y = <*n*> and
A18: f . y = n + 2 ; :: thesis: contradiction
0 + 1 = (n + 1) + 1 by A13, A17, A18;
hence contradiction ; :: thesis: verum

end;

now :: thesis: ( y = {} & f . y = 1 implies for n being Nat holds
( not x = <*n*> or not f . x = n + 2 ) )

assume that
y = {} and
A19: f . y = 1 ; :: thesis: for n being Nat holds
( not x = <*n*> or not f . x = n + 2 )
given n being Nat such that x = <*n*> and
A20: f . x = n + 2 ; :: thesis: contradiction
0 + 1 = (n + 1) + 1 by A13, A19, A20;
hence contradiction ; :: thesis: verum

end;

hence x = y by A13, A14, A15, A16; :: thesis: verum

end;

thus dom f = elementary_tree n by A10; :: thesis: rng f = Seg (n + 1)
thus rng f c= Seg (n + 1) :: according to XBOOLE_0:def 10 :: thesis: Seg (n + 1) is_a_prefix_of rng f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in Seg (n + 1) )
assume x in rng f ; :: thesis: x in Seg (n + 1)
then consider y being object such that
A21: y in dom f and
A22: x = f . y by FUNCT_1:def 3;
1 <= 1 + n by NAT_1:11;
then A23: 1 in Seg (n + 1) by FINSEQ_1:1;

now :: thesis: ( ex k being Nat st
( y = <*k*> & x = k + 2 ) implies x in Seg (n + 1) )

given k being Nat such that A24: y = <*k*> and
A25: x = k + 2 ; :: thesis: x in Seg (n + 1)
( y in { <*j*> where j is Nat : j < n } or y in {{}} ) by A10, A21, XBOOLE_0:def 3;
then consider l being Nat such that
A26: ( y = <*l*> & l < n ) by A24, TARSKI:def 1;
( <*k*> . 1 = k & <*l*> . 1 = l ) ;
then k + 1 <= n by A24, A26, NAT_1:13;
then ( 1 + 0 <= (k + 1) + 1 & (k + 1) + 1 <= n + 1 ) by XREAL_1:7;
hence x in Seg (n + 1) by A25, FINSEQ_1:1; :: thesis: verum

end;

hence x in Seg (n + 1) by A10, A21, A22, A23; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (n + 1) or x in rng f )
assume A27: x in Seg (n + 1) ; :: thesis: x in rng f
then reconsider k = x as Nat ;
A28: 1 <= k by A27, FINSEQ_1:1;
A29: k <= n + 1 by A27, FINSEQ_1:1;
{} in {{}} by TARSKI:def 1;
then A30: {} in elementary_tree n by XBOOLE_0:def 3;
then S₁[ {} ,f . {}] by A10;
then A31: 1 in rng f by A10, A30, FUNCT_1:def 3;

now :: thesis: ( 1 < k implies k in rng f )

assume 1 < k ; :: thesis: k in rng f
then 1 + 1 <= k by NAT_1:13;
then consider m being Nat such that
A32: k = 2 + m by NAT_1:10;
reconsider m = m as Nat ;
(1 + 1) + m = 1 + (1 + m) ;
then 1 + m <= n by A29, A32, XREAL_1:6;
then m < n by NAT_1:13;
then <*m*> in { <*j*> where j is Nat : j < n } ;
then A33: <*m*> in elementary_tree n by XBOOLE_0:def 3;
then S₁[<*m*>,f . <*m*>] by A10;
then k = f . <*m*> by A1, A32, A33;
hence k in rng f by A10, A33, FUNCT_1:def 3; :: thesis: verum

end;

hence x in rng f by A28, A31, XXREAL_0:1; :: thesis: verum

end;

hence elementary_tree n is finite by CARD_1:38; :: thesis: verum