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

A1: now

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 A3: x in { <*k*> where k is Element of NAT : k < n + 1 } ; :: thesis:
A4: ex k being Element of NAT st
( x = <*k*> & k < n + 1 ) by A3;
thus x is FinSequence by A4; :: thesis:

end;

let p1, p2 be FinSequence; :: thesis:
assume A5: ( 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:
A6: ( ex k being Element of NAT st
( p1 = <*k*> & k < n + 1 ) & ex m being Element of NAT st
( p2 = <*m*> & m < n + 1 ) ) by A5;
thus ( not p1 <> p2 or not p1,p2 are_c=-comparable ) by A6, Th23; :: thesis:

end;

reconsider X = { <*k*> where k is Element of NAT : k < n + 1 } as AntiChain_of_Prefixes by A2;
A7: X c= elementary_tree (n + 1) by XBOOLE_1:7;
reconsider X = X as AntiChain_of_Prefixes of elementary_tree (n + 1) by A7, Def14;
take X = X; :: thesis:
A8: 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:
A12: <*n1*> . 1 = n1 by FINSEQ_1:def 8;
thus y = z by A10, A11, A12, 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 A14: x in X ; :: thesis:
consider k being Element of NAT such that
A15: x = <*k*> and
k < n + 1 by A14;
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:
A19: ( 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;
thus x = y by A18, A19; :: thesis:

end;

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

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A20: x in rng f ; :: thesis:
consider y being set such that
A21: y in dom f and
A22: x = f . y by A20, 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;
A26: ( <*k*> . 1 = k & <*m*> . 1 = m ) by FINSEQ_1:def 8;
A27: ( 0 + 1 <= k + 1 & k + 1 <= n + 1 ) by A23, A25, A26, NAT_1:13;
thus x in Seg (n + 1) by A24, A27, FINSEQ_1:3; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A28: x in Seg (n + 1) ; :: thesis:
reconsider k = x as Element of NAT by A28;
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;
A32: m < n + 1 by A30, A31, NAT_1:13;
A33: <*m*> in X by A32;
A34: S₁[<*m*>,f . <*m*>] by A16, A33;
A35: x = f . <*m*> by A9, A31, A33, A34;
thus x in rng f by A16, A33, A35, FUNCT_1:def 5; :: thesis:

end;

A36: card (Seg (n + 1)) = card X by A8, CARD_1:21;
thus n + 1 = card X by A36, FINSEQ_1:78; :: thesis:
let Y be AntiChain_of_Prefixes of elementary_tree (n + 1); :: thesis:
A37: Y c= elementary_tree (n + 1) by Def14;
A38: ( {} in Y implies Y = {{} } )

assume that
A39: {} in Y and
A40: Y <> {{} } ; :: thesis:
consider x being set such that
A41: ( ( x in Y & not x in {{} } ) or ( x in {{} } & not x in Y ) ) by A40, TARSKI:2;
A42: {} <> x by A39, A41, TARSKI:def 1;
reconsider x = x as FinSequence of NAT by A37, A39, A41, Th44, TARSKI:def 1;
A43: {} is_a_prefix_of x by XBOOLE_1:2;
A44: {} ,x are_c=-comparable by A43, XBOOLE_0:def 9;
thus contradiction by A39, A41, A42, A44, Def13, TARSKI:def 1; :: thesis:

end;

A45: ( card {{} } = 1 & 1 <= 1 + n ) by CARD_1:50, NAT_1:11;

A46: now

assume A47: not {} in Y ; :: thesis:
A48: Y c= X

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A49: x in Y ; :: thesis:
A50: ( x in { <*k*> where k is Element of NAT : k < n + 1 } or x in {{} } ) by A37, A49, XBOOLE_0:def 3;
thus x in X by A47, A49, A50, TARSKI:def 1; :: thesis:

end;

thus card Y <= card X by A48, NAT_1:44; :: thesis:

end;

thus card Y <= card X by A36, A38, A45, A46, FINSEQ_1:78; :: thesis:

end;

thus width (elementary_tree (n + 1)) = n + 1 by A1, Def16; :: thesis: