defpred S₁[ object ] means ( $1 = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & $1 = <*n*> ^ q ) );
consider T being set such that
A2: for y being object holds
( y in T iff ( y in NAT * & S₁[y] ) ) from XBOOLE_0:sch 1();
<*> NAT in NAT * by FINSEQ_1:def 11;
then reconsider T = T as non empty set by A2;
A3: rng p is constituted-Trees by A1;
then A4: for n being Nat st n < len p holds
p . (n + 1) is Tree by Lm3;
T is Tree-like

proof

thus T c= NAT * by A2; :: according to TREES_1:def 3 :: thesis: ( ( for b₁ being FinSequence of NAT holds
( not b₁ in T or ProperPrefixes b₁ c= T ) ) & ( for b₁ being FinSequence of NAT
for b₂, b₃ being set holds
( not b₁ ^ <*b₂*> in T or not b₃ <= b₂ or b₁ ^ <*b₃*> in T ) ) )
thus for w being FinSequence of NAT st w in T holds
ProperPrefixes w c= T :: thesis: for b₁ being FinSequence of NAT
for b₂, b₃ being set holds
( not b₁ ^ <*b₂*> in T or not b₃ <= b₂ or b₁ ^ <*b₃*> in T )

proof

let w be FinSequence of NAT ; :: thesis: ( w in T implies ProperPrefixes w c= T )
assume A5: w in T ; :: thesis: ProperPrefixes w c= T

now :: thesis: ( w <> {} implies ProperPrefixes w c= T )

assume w <> {} ; :: thesis: ProperPrefixes w c= T
then consider n being Nat, q being FinSequence such that
A6: n < len p and
A7: q in p . (n + 1) and
A8: w = <*n*> ^ q by A2, A5;
reconsider q = q as FinSequence of NAT by A8, FINSEQ_1:36;
thus ProperPrefixes w c= T :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes w or x in T )
assume x in ProperPrefixes w ; :: thesis: x in T
then consider r being FinSequence such that
A9: x = r and
A10: r is_a_proper_prefix_of w by TREES_1:def 2;
r is_a_prefix_of w by A10;
then consider k being Nat such that
A11: r = w | (Seg k) ;
rng r = w .: (Seg k) by A11, RELAT_1:115;
then reconsider r = r as FinSequence of NAT by FINSEQ_1:def 4;
A12: r in NAT * by FINSEQ_1:def 11;

now :: thesis: ( r <> {} implies x in T )

assume r <> {} ; :: thesis: x in T
then consider r1 being FinSequence of NAT , i being Element of NAT such that
A13: r = <*i*> ^ r1 by FINSEQ_2:130;
A14: dom <*i*> = Seg 1 by FINSEQ_1:38;
A15: 1 in Seg 1 by FINSEQ_1:2, TARSKI:def 1;
A16: Seg 1 c= dom r by A13, A14, FINSEQ_1:26;
A17: r . 1 = i by A13, FINSEQ_1:41;
A18: w . 1 = n by A8, FINSEQ_1:41;
A19: r . 1 = w . 1 by A11, A15, A16, FUNCT_1:47;
then A20: r1 is_a_proper_prefix_of q by A8, A10, A13, A17, A18, TREES_1:49;
A21: p . (n + 1) is Tree by A4, A6;
r1 is_a_prefix_of q by A20;
then r1 in p . (n + 1) by A7, A21, TREES_1:20;
hence x in T by A2, A6, A9, A12, A13, A17, A18, A19; :: thesis: verum

end;

hence x in T by A2, A9, A12; :: thesis: verum

end;

end;

hence ProperPrefixes w c= T by TREES_1:15; :: thesis: verum

end;

let w be FinSequence of NAT ; :: thesis: for b₁, b₂ being set holds
( not w ^ <*b₁*> in T or not b₂ <= b₁ or w ^ <*b₂*> in T )
let k, n be Nat; :: thesis: ( not w ^ <*k*> in T or not n <= k or w ^ <*n*> in T )
assume that
A22: w ^ <*k*> in T and
A23: n <= k ; :: thesis: w ^ <*n*> in T

A24: now :: thesis: ( w = {} implies w ^ <*n*> in T )

assume A25: w = {} ; :: thesis: w ^ <*n*> in T
then <*k*> in T by A22, FINSEQ_1:34;
then consider m being Nat, q being FinSequence such that
A26: m < len p and
q in p . (m + 1) and
A27: <*k*> = <*m*> ^ q by A2;
(<*m*> ^ q) . 1 = m by FINSEQ_1:41;
then A29: n < len p by A23, A26, A27, XXREAL_0:2;
then p . (n + 1) in rng p by Lm3;
then A30: {} in p . (n + 1) by A3, TREES_1:22;
A31: <*n*> ^ {} = <*n*> by FINSEQ_1:34;
A32: {} ^ <*n*> = <*n*> by FINSEQ_1:34;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
<*n*> in NAT * by FINSEQ_1:def 11;
hence w ^ <*n*> in T by A2, A25, A29, A30, A31, A32; :: thesis: verum

end;

now :: thesis: ( w <> {} implies w ^ <*n*> in T )

assume w <> {} ; :: thesis: w ^ <*n*> in T
then consider q being FinSequence of NAT , m being Element of NAT such that
A33: w = <*m*> ^ q by FINSEQ_2:130;
consider m9 being Nat, r being FinSequence such that
A34: m9 < len p and
A35: r in p . (m9 + 1) and
A36: w ^ <*k*> = <*m9*> ^ r by A2, A22;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A37: w ^ <*k*> = <*m*> ^ (q ^ <*k*>) by A33, FINSEQ_1:32;
A38: w ^ <*n*> = <*m*> ^ (q ^ <*n*>) by A33, FINSEQ_1:32;
A39: (w ^ <*k*>) . 1 = m by A37, FINSEQ_1:41;
A40: (w ^ <*k*>) . 1 = m9 by A36, FINSEQ_1:41;
A41: <*m*> ^ (q ^ <*n*>) in NAT * by FINSEQ_1:def 11;
A42: r = q ^ <*k*> by A36, A37, A39, A40, FINSEQ_1:33;
p . (m + 1) in rng p by A34, A39, A40, Lm3;
then q ^ <*n*> in p . (m + 1) by A3, A23, A35, A39, A40, A42, TREES_1:def 3;
hence w ^ <*n*> in T by A2, A34, A38, A39, A40, A41; :: thesis: verum

end;

hence w ^ <*n*> in T by A24; :: thesis: verum

end;

then reconsider T = T as Tree ;
take T ; :: thesis: for x being object holds
( x in T iff ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) )
let x be object ; :: thesis: ( x in T iff ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) )
thus ( not x in T or x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) by A2; :: thesis: ( ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) implies x in T )
assume A43: ( x = {} or ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) ) ; :: thesis: x in T

A44: now :: thesis: ( ex n being Nat ex q being FinSequence st
( n < len p & q in p . (n + 1) & x = <*n*> ^ q ) implies x in NAT * )

given n being Nat, q being FinSequence such that A45: n < len p and
A46: q in p . (n + 1) and
A47: x = <*n*> ^ q ; :: thesis: x in NAT *
reconsider T1 = p . (n + 1) as Tree by A4, A45;
reconsider q = q as Element of T1 by A46;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
<*n*> ^ q in NAT * by FINSEQ_1:def 11;
hence x in NAT * by A47; :: thesis: verum

end;

{} in NAT * by FINSEQ_1:49;
hence x in T by A2, A43, A44; :: thesis: verum