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 & len p >= k ) by A5, A6, A7, XXREAL_0:2;
reconsider q = p | (Seg k) as FinSequence by FINSEQ_1:19;
A10: len q = k by A9, FINSEQ_1:21;
then A11: ( ProperPrefixes q is finite & card (ProperPrefixes q) = k ) by TREES_1:68;
then card (ProperPrefixes q) in card C by A8, NAT_1:45;
then A12: C \ (ProperPrefixes q) <> {} by CARD_2:4;
consider x being Element of C \ (ProperPrefixes q);
A13: ( x in C & not x in ProperPrefixes q ) by A12, XBOOLE_0:def 5;
then reconsider x = x as Element of W ;
( card ((ProperPrefixes q) \/ {x}) = k + 1 & (ProperPrefixes q) \/ {x} is finite ) by A11, A13, CARD_2:54;
then card ((ProperPrefixes q) \/ {x}) in card C by A6, NAT_1:45;
then A14: C \ ((ProperPrefixes q) \/ {x}) <> {} by CARD_2:4;
consider y being Element of C \ ((ProperPrefixes q) \/ {x});
A15: ( y in C & not y in (ProperPrefixes q) \/ {x} ) by A14, XBOOLE_0:def 5;
then reconsider y = y as Element of W ;
( not y in ProperPrefixes q & not y in {x} & q is_a_prefix_of p ) by A15, TREES_1:def 1, XBOOLE_0:def 3;
then ( q is_a_prefix_of x & q is_a_prefix_of y & x <> y & ( x = q or x <> q ) ) by A9, A13, A15, Th24, TARSKI:def 1;
then ( q is_a_proper_prefix_of y or q is_a_proper_prefix_of x ) by XBOOLE_0:def 8;
then ( k < len x or k < len y ) by A10, 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 A13, A15; :: 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