let W be Tree; for n being 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 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 C be finite Chain of W; ( card C > n implies ex p being FinSequence of NAT st
( p in C & len p >= n ) )
defpred S1[ Nat] means ( $1 < card C implies ex p being FinSequence of NAT st
( p in C & len p >= $1 ) );
A1:
S1[ 0 ]
A4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[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
;
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:15;
A11:
len q = k
by A10, FINSEQ_1:17;
then A12:
card (ProperPrefixes q) = k
by TREES_1:35;
then
card (ProperPrefixes q) in Segm (card C)
by A8, NAT_1:44;
then A13:
C \ (ProperPrefixes q) <> {}
by CARD_1:68;
set x = the
Element of
C \ (ProperPrefixes q);
A14:
the
Element of
C \ (ProperPrefixes q) in C
by A13, XBOOLE_0:def 5;
A15:
not the
Element of
C \ (ProperPrefixes q) in ProperPrefixes q
by A13, XBOOLE_0:def 5;
reconsider x = the
Element of
C \ (ProperPrefixes q) as
Element of
W by A14;
card ((ProperPrefixes q) \/ {x}) = k + 1
by A12, A15, CARD_2:41;
then
card ((ProperPrefixes q) \/ {x}) in Segm (card C)
by A6, NAT_1:44;
then A16:
C \ ((ProperPrefixes q) \/ {x}) <> {}
by CARD_1:68;
set y = the
Element of
C \ ((ProperPrefixes q) \/ {x});
A17:
the
Element of
C \ ((ProperPrefixes q) \/ {x}) in C
by A16, XBOOLE_0:def 5;
A18:
not the
Element of
C \ ((ProperPrefixes q) \/ {x}) in (ProperPrefixes q) \/ {x}
by A16, XBOOLE_0:def 5;
reconsider y = the
Element of
C \ ((ProperPrefixes q) \/ {x}) as
Element of
W by A17;
A19:
not
y in ProperPrefixes q
by A18, XBOOLE_0:def 3;
A20:
not
y in {x}
by A18, XBOOLE_0:def 3;
A21:
q is_a_prefix_of p
;
then A22:
q is_a_prefix_of x
by A9, A14, A15, Th22;
A23:
q is_a_prefix_of y
by A9, A17, A19, A21, Th22;
A24:
x <> y
by A20, TARSKI:def 1;
(
q is_a_proper_prefix_of y or
q is_a_proper_prefix_of x )
by A22, A23, A24;
then
(
k < len x or
k < len y )
by A11, TREES_1:6;
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 A14, A17;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A4);
hence
( card C > n implies ex p being FinSequence of NAT st
( p in C & len p >= n ) )
; verum