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 ) );
A34: ( 0 = card {} & ( for p, q being FinSequence of NAT st p in {} & q in {} & p <> q holds
not p,q are_c=-comparable ) ) ;
A35: ex n being Nat st S₁[n] by A34, XBOOLE_1:2;
A36: 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 A37: ( 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
A38: ( card X c= card T & card X = card n ) by A37, CARD_1:27;
A39: card T = card (card T) ;
thus n <= card T by A38, A39, NAT_1:41; :: thesis: verum

end;

consider n being Nat such that
A40: S₁[n] and
A41: for m being Nat st S₁[m] holds
m <= n from NAT_1:sch 6(A36, A35);
consider X being finite set such that
A42: n = card X and
A43: X c= T and
A44: for p, q being FinSequence of NAT st p in X & q in X & p <> q holds
not p,q are_c=-comparable by A40;
A45: 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 13 :: 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 A46: x in X ; :: thesis: x is FinSequence
A47: x in T by A43, A46;
A48: T c= NAT * by Def5;
thus x is FinSequence by A47, A48, FINSEQ_1:def 11; :: 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 A49: ( p1 in X & p2 in X ) ; :: thesis: ( not p1 <> p2 or not p1,p2 are_c=-comparable )
reconsider q1 = p1, q2 = p2 as Element of T by A43, A49;
A50: ( p1 = q1 & p2 = q2 ) ;
thus ( not p1 <> p2 or not p1,p2 are_c=-comparable ) by A44, A49, A50; :: thesis: verum

end;

reconsider X = X as AntiChain_of_Prefixes by A45;
reconsider X = X as AntiChain_of_Prefixes of T by A43, Def14;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
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 A42; :: 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
A51: ( 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 Def13, Def14;
thus card Y <= card X by A41, A42, A51; :: thesis: verum