let n be Element of NAT ; :: thesis:
set T = elementary_tree (n + 1);

thus for x being set st x in { <*k*> where k is Element of NAT : k < n + 1 } holds
x is FinSequence :: according to TREES_1:def 13 :: thesis:

let x be set ; :: thesis:
assume x in { <*k*> where k is Element of NAT : k < n + 1 } ; :: thesis:
then ex k being Element of NAT st
( x = <*k*> & k < n + 1 ) ;
hence x is FinSequence ; :: thesis:

end;

let p1, p2 be FinSequence; :: thesis:
assume ( p1 in { <*k*> where k is Element of NAT : k < n + 1 } & p2 in { <*m*> where m is Element of NAT : m < n + 1 } ) ; :: thesis:
then ( ex k being Element of NAT st
( p1 = <*k*> & k < n + 1 ) & ex m being Element of NAT st
( p2 = <*m*> & m < n + 1 ) ) ;
hence ( not p1 <> p2 or not p1,p2 are_c=-comparable ) by Th23; :: thesis:

end;

then reconsider X = { <*k*> where k is Element of NAT : k < n + 1 } as AntiChain_of_Prefixes ;
X c= elementary_tree (n + 1) by XBOOLE_1:7;
then reconsider X = X as AntiChain_of_Prefixes of elementary_tree (n + 1) by Def14;
take X = X; :: thesis:
X, Seg (n + 1) are_equipotent

defpred S₁[ set , set ] means ex n being Element of NAT st
( $1 = <*n*> & $2 = n + 1 );
A9: for x, y, z being set st x in X & S₁[x,y] & S₁[x,z] holds
y = z

let x, y, z be set ; :: thesis:
assume x in X ; :: thesis:
given n1 being Element of NAT such that A10: ( x = <*n1*> & y = n1 + 1 ) ; :: thesis:
given n2 being Element of NAT such that A11: ( x = <*n2*> & z = n2 + 1 ) ; :: thesis:
<*n1*> . 1 = n1 by FINSEQ_1:def 8;
hence y = z by A10, A11, FINSEQ_1:def 8; :: thesis:

end;

A13: for x being set st x in X holds
ex y being set st S₁[x,y]

let x be set ; :: thesis:
assume x in X ; :: thesis:
then consider k being Element of NAT such that
A15: x = <*k*> and
k < n + 1 ;
reconsider y = k + 1 as set ;
take y ; :: thesis:
thus S₁[x,y] by A15; :: thesis:

end;

consider f being Function such that
A16: ( dom f = X & ( for x being set st x in X holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A13);
take f ; :: according to WELLORD2:def 4 :: thesis:
thus f is one-to-one :: thesis:

let x be set ; :: according to FUNCT_1:def 8 :: thesis:
let y be set ; :: thesis:
assume that
A17: ( x in dom f & y in dom f ) and
A18: f . x = f . y ; :: thesis:
( ex k1 being Element of NAT st
( x = <*k1*> & f . x = k1 + 1 ) & ex k2 being Element of NAT st
( y = <*k2*> & f . y = k2 + 1 ) ) by A16, A17;
hence x = y by A18; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being set such that
A21: y in dom f and
A22: x = f . y by FUNCT_1:def 5;
consider k being Element of NAT such that
A23: y = <*k*> and
A24: x = k + 1 by A16, A21, A22;
consider m being Element of NAT such that
A25: ( y = <*m*> & m < n + 1 ) by A16, A21;
( <*k*> . 1 = k & <*m*> . 1 = m ) by FINSEQ_1:def 8;
then ( 0 + 1 <= k + 1 & k + 1 <= n + 1 ) by A23, A25, NAT_1:13;
hence x in Seg (n + 1) by A24, FINSEQ_1:3; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A28: x in Seg (n + 1) ; :: thesis:
then reconsider k = x as Element of NAT ;
A29: 1 <= k by A28, FINSEQ_1:3;
A30: k <= n + 1 by A28, FINSEQ_1:3;
consider m being Nat such that
A31: k = 1 + m by A29, NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
m < n + 1 by A30, A31, NAT_1:13;
then A33: <*m*> in X ;
then S₁[<*m*>,f . <*m*>] by A16;
then x = f . <*m*> by A9, A31, A33;
hence x in proj2 f by A16, A33, FUNCT_1:def 5; :: thesis:

end;

end;

end;

end;

end;