set X = {0,1} * ;

hence {0,1} * is Tree by A1, A5, TREES_1:def 3; :: thesis: verum

A1: now :: thesis: for p being FinSequence of NAT st p in {0,1} * holds

ProperPrefixes p c= {0,1} *

ProperPrefixes p c= {0,1} *

let p be FinSequence of NAT ; :: thesis: ( p in {0,1} * implies ProperPrefixes p c= {0,1} * )

assume A2: p in {0,1} * ; :: thesis: ProperPrefixes p c= {0,1} *

thus ProperPrefixes p c= {0,1} * :: thesis: verum

end;assume A2: p in {0,1} * ; :: thesis: ProperPrefixes p c= {0,1} *

thus ProperPrefixes p c= {0,1} * :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ProperPrefixes p or y in {0,1} * )

assume y in ProperPrefixes p ; :: thesis: y in {0,1} *

then consider q being FinSequence such that

A3: y = q and

A4: q is_a_proper_prefix_of p by TREES_1:def 2;

q is_a_prefix_of p by A4;

then ex n being Nat st q = p | (Seg n) by TREES_1:def 1;

hence y in {0,1} * by A2, A3, Th1; :: thesis: verum

end;assume y in ProperPrefixes p ; :: thesis: y in {0,1} *

then consider q being FinSequence such that

A3: y = q and

A4: q is_a_proper_prefix_of p by TREES_1:def 2;

q is_a_prefix_of p by A4;

then ex n being Nat st q = p | (Seg n) by TREES_1:def 1;

hence y in {0,1} * by A2, A3, Th1; :: thesis: verum

A5: now :: thesis: for p being FinSequence of NAT

for k, n being Nat st p ^ <*k*> in {0,1} * & n <= k holds

p ^ <*n*> in {0,1} *

{0,1} * c= NAT *
by FINSEQ_1:62;for k, n being Nat st p ^ <*k*> in {0,1} * & n <= k holds

p ^ <*n*> in {0,1} *

let p be FinSequence of NAT ; :: thesis: for k, n being Nat st p ^ <*k*> in {0,1} * & n <= k holds

p ^ <*n*> in {0,1} *

let k, n be Nat; :: thesis: ( p ^ <*k*> in {0,1} * & n <= k implies p ^ <*n*> in {0,1} * )

assume that

A6: p ^ <*k*> in {0,1} * and

A7: n <= k ; :: thesis: p ^ <*n*> in {0,1} *

A8: p ^ <*k*> is FinSequence of {0,1} by A6, FINSEQ_1:def 11;

then reconsider kk = <*k*> as FinSequence of {0,1} by FINSEQ_1:36;

1 in Seg 1 by FINSEQ_1:3;

then 1 in dom <*k*> by FINSEQ_1:38;

then kk . 1 in {0,1} by FINSEQ_2:11;

then A9: k in {0,1} by FINSEQ_1:40;

then n in {0,1} by TARSKI:def 2;

then A11: <*n*> is FinSequence of {0,1} by Lm2;

p is FinSequence of {0,1} by A8, FINSEQ_1:36;

then p ^ <*n*> is FinSequence of {0,1} by A11, Lm1;

hence p ^ <*n*> in {0,1} * by FINSEQ_1:def 11; :: thesis: verum

end;p ^ <*n*> in {0,1} *

let k, n be Nat; :: thesis: ( p ^ <*k*> in {0,1} * & n <= k implies p ^ <*n*> in {0,1} * )

assume that

A6: p ^ <*k*> in {0,1} * and

A7: n <= k ; :: thesis: p ^ <*n*> in {0,1} *

A8: p ^ <*k*> is FinSequence of {0,1} by A6, FINSEQ_1:def 11;

then reconsider kk = <*k*> as FinSequence of {0,1} by FINSEQ_1:36;

1 in Seg 1 by FINSEQ_1:3;

then 1 in dom <*k*> by FINSEQ_1:38;

then kk . 1 in {0,1} by FINSEQ_2:11;

then A9: k in {0,1} by FINSEQ_1:40;

then n in {0,1} by TARSKI:def 2;

then A11: <*n*> is FinSequence of {0,1} by Lm2;

p is FinSequence of {0,1} by A8, FINSEQ_1:36;

then p ^ <*n*> is FinSequence of {0,1} by A11, Lm1;

hence p ^ <*n*> in {0,1} * by FINSEQ_1:def 11; :: thesis: verum

hence {0,1} * is Tree by A1, A5, TREES_1:def 3; :: thesis: verum