defpred S₁[ Nat] means ex X being finite set st
( $1 = card X & X c= T & ( for p, q being FinSequence of NAT st p in X & q in X & p <> q holds
not p,q are_c=-comparable ) );
( 0 = card {} & ( for p, q being FinSequence of NAT st p in {} & q in {} & p <> q holds
not p,q are_c=-comparable ) ) ;
then A21: ex n being Nat st S₁[n] by XBOOLE_1:2;
A22: for n being Nat st S₁[n] holds
n <= card T

proof

let n be Nat; :: thesis:
given X being finite set such that A23: ( n = card X & X c= T ) and
for p, q being FinSequence of NAT st p in X & q in X & p <> q holds
not p,q are_c=-comparable ; :: thesis:
A24: ( Segm (card X) c= Segm (card T) & card X = card n ) by A23, CARD_1:11;
card T = card (Segm (card T)) ;
hence n <= card T by A24, NAT_1:40; :: thesis:

end;

consider n being Nat such that
A25: S₁[n] and
A26: for m being Nat st S₁[m] holds
m <= n from NAT_1:sch 6(A22, A21);
consider X being finite set such that
A27: n = card X and
A28: X c= T and
A29: for p, q being FinSequence of NAT st p in X & q in X & p <> q holds
not p,q are_c=-comparable by A25;
X is AntiChain_of_Prefixes-like

proof

thus for x being set st x in X holds
x is FinSequence :: according to TREES_1:def 10 :: thesis:

proof

let x be set ; :: thesis:
assume A30: x in X ; :: thesis:
T c= NAT * by Def3;
hence x is FinSequence by A30, A28; :: thesis:

end;

let p1, p2 be FinSequence; :: thesis:
assume A31: ( p1 in X & p2 in X ) ; :: thesis:
then reconsider q1 = p1, q2 = p2 as Element of T by A28;
( p1 = q1 & p2 = q2 ) ;
hence ( not p1 <> p2 or not p1,p2 are_c=-comparable ) by A29, A31; :: thesis:

end;

then reconsider X = X as AntiChain_of_Prefixes ;
reconsider X = X as AntiChain_of_Prefixes of T by A28, Def11;
reconsider n = n as Nat ;
take n ; :: thesis:
take X ; :: thesis:
thus n = card X by A27; :: thesis:
let Y be AntiChain_of_Prefixes of T; :: thesis:
( Y c= T & ( for p, q being FinSequence of NAT st p in Y & q in Y & p <> q holds
not p,q are_c=-comparable ) ) by Def10, Def11;
hence card Y <= card X by A26, A27; :: thesis: