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: ( S₁[n] implies n <= card T )
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: n <= card T
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: verum

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: for p1, p2 being FinSequence st p1 in X & p2 in X & p1 <> p2 holds
not p1,p2 are_c=-comparable

proof

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

end;

let p1, p2 be FinSequence; :: thesis: ( p1 in X & p2 in X & p1 <> p2 implies not p1,p2 are_c=-comparable )
assume A31: ( p1 in X & p2 in X ) ; :: thesis: ( not p1 <> p2 or not p1,p2 are_c=-comparable )
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: verum

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: ex X being AntiChain_of_Prefixes of T st
( n = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) )
take X ; :: thesis: ( n = card X & ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) )
thus n = card X by A27; :: thesis: for Y being AntiChain_of_Prefixes of T holds card Y <= card X
let Y be AntiChain_of_Prefixes of T; :: thesis: card Y <= card X
( 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: verum