let T be Tree; :: thesis: for B being Branch of
for t being Element of T st t in B & not B is finite holds
ex t' being Element of T st
( t' in B & t' in succ t )
let B be Branch of ; :: thesis: for t being Element of T st t in B & not B is finite holds
ex t' being Element of T st
( t' in B & t' in succ t )
let t be Element of T; :: thesis: ( t in B & not B is finite implies ex t' being Element of T st
( t' in B & t' in succ t ) )
assume ( t in B & not B is finite ) ; :: thesis: ex t' being Element of T st
( t' in B & t' in succ t )
then consider t'' being Element of T such that
A1: t'' in B and
A2: t is_a_proper_prefix_of t'' by Th23;
t is_a_prefix_of t'' by A2, XBOOLE_0:def 8;
then consider r being FinSequence such that
A3: t'' = t ^ r by TREES_1:8;
reconsider r = r as FinSequence of NAT by A3, FINSEQ_1:50;
r | (Seg 1) is FinSequence of NAT by FINSEQ_1:23;
then consider r1 being FinSequence of NAT such that
A4: r1 = r | (Seg 1) ;
1 <= len r

proof

len t < len t'' by A2, TREES_1:24;
then consider m being Nat such that
A5: (len t) + m = len t'' by NAT_1:10;
m <> 0 by A2, A5, TREES_1:24;
then 0 < m by NAT_1:3;
then A6: 0 + 1 <= m by NAT_1:13;
len t'' = (len t) + (len r) by A3, FINSEQ_1:35;
hence 1 <= len r by A5, A6; :: thesis: verum

end;

then consider n being Element of NAT such that
A7: r1 = <*n*> by A4, Th7;
A8: r1 is_a_prefix_of r by A4, TREES_1:def 1;
then A9: t ^ r1 is_a_prefix_of t'' by A3, FINSEQ_6:15;
t ^ <*n*> in T by A3, A7, A8, FINSEQ_6:15, TREES_1:45;
then consider t' being Element of T such that
A10: t' = t ^ <*n*> ;
t' in succ t by A10;
hence ex t' being Element of T st
( t' in B & t' in succ t ) by A1, A7, A9, A10, TREES_2:27; :: thesis: verum