let n be Nat; :: thesis:
set T = elementary_tree (n + 1);

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

let x be set ; :: thesis:
assume x in { <*k*> where k is Nat : k < n + 1 } ; :: thesis:
then ex k being 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 Nat : k < n + 1 } & p2 in { <*m*> where m is Nat : m < n + 1 } ) ; :: thesis:
then ( ex k being Nat st
( p1 = <*k*> & k < n + 1 ) & ex m being Nat st
( p2 = <*m*> & m < n + 1 ) ) ;
hence ( not p1 <> p2 or not p1,p2 are_c=-comparable ) by Th4; :: thesis:

end;

then reconsider X = { <*k*> where k is 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 Def11;
take X = X; :: thesis:
X, Seg (n + 1) are_equipotent

defpred S₁[ object , object ] means ex n being Nat st
( $1 = <*n*> & $2 = n + 1 );
A1: 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 Nat such that A2: ( x = <*n1*> & y = n1 + 1 ) ; :: thesis:
given n2 being Nat such that A3: ( x = <*n2*> & z = n2 + 1 ) ; :: thesis:
<*n1*> . 1 = n1 ;
hence y = z by A2, A3, FINSEQ_1:def 8; :: thesis:

end;

A4: for x being object st x in X holds
ex y being object st S₁[x,y]

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

end;

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

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A7: ( x in dom f & y in dom f ) and
A8: f . x = f . y ; :: thesis:
( ex k1 being Nat st
( x = <*k1*> & f . x = k1 + 1 ) & ex k2 being Nat st
( y = <*k2*> & f . y = k2 + 1 ) ) by A6, A7;
hence x = y by A8; :: thesis:

end;

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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng f ; :: thesis:
then consider y being object such that
A9: y in dom f and
A10: x = f . y by FUNCT_1:def 3;
consider k being Nat such that
A11: y = <*k*> and
A12: x = k + 1 by A6, A9, A10;
consider m being Nat such that
A13: ( y = <*m*> & m < n + 1 ) by A6, A9;
( <*k*> . 1 = k & <*m*> . 1 = m ) ;
then ( 0 + 1 <= k + 1 & k + 1 <= n + 1 ) by A11, A13, NAT_1:13;
hence x in Seg (n + 1) by A12, FINSEQ_1:1; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: x in Seg (n + 1) ; :: thesis:
then reconsider k = x as Nat ;
A15: 1 <= k by A14, FINSEQ_1:1;
A16: k <= n + 1 by A14, FINSEQ_1:1;
consider m being Nat such that
A17: k = 1 + m by A15, NAT_1:10;
reconsider m = m as Nat ;
m < n + 1 by A16, A17, NAT_1:13;
then A18: <*m*> in X ;
then S₁[<*m*>,f . <*m*>] by A6;
then x = f . <*m*> by A1, A17, A18;
hence x in rng f by A6, A18, FUNCT_1:def 3; :: thesis:

end;

end;

end;

end;

end;