let W be Tree; :: thesis: for n being Element of NAT
for C being finite Chain of W st card C > n holds
ex p being FinSequence of NAT st
( p in C & len p >= n )
let n be Element of NAT ; :: thesis: for C being finite Chain of W st card C > n holds
ex p being FinSequence of NAT st
( p in C & len p >= n )
let C be finite Chain of W; :: thesis: ( card C > n implies ex p being FinSequence of NAT st
( p in C & len p >= n ) )
defpred S₁[ Element of NAT ] means ( $1 < card C implies ex p being FinSequence of NAT st
( p in C & len p >= $1 ) );
A1: S₁[ 0 ]

proof

assume A2: 0 < card C ; :: thesis: ex p being FinSequence of NAT st
( p in C & len p >= 0 )
then A3: C <> {} ;
consider x being Element of C;
reconsider x = x as Element of W by A2, CARD_1:47, TARSKI:def 3;
reconsider x = x as FinSequence of NAT ;
take x ; :: thesis: ( x in C & len x >= 0 )
thus ( x in C & len x >= 0 ) by A3; :: thesis: verum

end;

A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume that
A5: ( k < card C implies ex p being FinSequence of NAT st
( p in C & len p >= k ) ) and
A6: k + 1 < card C ; :: thesis: ex p being FinSequence of NAT st
( p in C & len p >= k + 1 )
A7: k <= k + 1 by NAT_1:11;
then A8: k < card C by A6, XXREAL_0:2;
consider p being FinSequence of NAT such that
A9: p in C and
A10: len p >= k by A5, A6, A7, XXREAL_0:2;
reconsider q = p | (Seg k) as FinSequence by FINSEQ_1:19;
A11: len q = k by A10, FINSEQ_1:21;
then A12: card (ProperPrefixes q) = k by TREES_1:68;
then card (ProperPrefixes q) in card C by A8, NAT_1:45;
then A14: C \ (ProperPrefixes q) <> {} by CARD_2:4;
consider x being Element of C \ (ProperPrefixes q);
A15: x in C by A14, XBOOLE_0:def 5;
A16: not x in ProperPrefixes q by A14, XBOOLE_0:def 5;
reconsider x = x as Element of W by A15;
card ((ProperPrefixes q) \/ {x}) = k + 1 by A12, A16, CARD_2:54;
then card ((ProperPrefixes q) \/ {x}) in card C by A6, NAT_1:45;
then A19: C \ ((ProperPrefixes q) \/ {x}) <> {} by CARD_2:4;
consider y being Element of C \ ((ProperPrefixes q) \/ {x});
A20: y in C by A19, XBOOLE_0:def 5;
A21: not y in (ProperPrefixes q) \/ {x} by A19, XBOOLE_0:def 5;
reconsider y = y as Element of W by A20;
A22: not y in ProperPrefixes q by A21, XBOOLE_0:def 3;
A23: not y in {x} by A21, XBOOLE_0:def 3;
A24: q is_a_prefix_of p by TREES_1:def 1;
then A25: q is_a_prefix_of x by A9, A15, A16, Th24;
A26: q is_a_prefix_of y by A9, A20, A22, A24, Th24;
A27: x <> y by A23, TARSKI:def 1;
( x = q or x <> q ) ;
then ( q is_a_proper_prefix_of y or q is_a_proper_prefix_of x ) by A25, A26, A27, XBOOLE_0:def 8;
then ( k < len x or k < len y ) by A11, TREES_1:24;
then ( k + 1 <= len x or k + 1 <= len y ) by NAT_1:13;
hence ex p being FinSequence of NAT st
( p in C & len p >= k + 1 ) by A15, A20; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A1, A4);
hence ( card C > n implies ex p being FinSequence of NAT st
( p in C & len p >= n ) ) ; :: thesis: verum