set X = {0 ,1} * ;

A1: now

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

proof

let y be set ; :: 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 4;
q is_a_prefix_of p by A4, XBOOLE_0:def 8;
then ex n being Element of NAT st q = p | (Seg n) by TREES_1:def 1;
hence y in {0 ,1} * by A2, A3, Th1; :: thesis: verum

end;

end;

A5: now

let p be FinSequence of NAT ; :: thesis: for k, n being Element of NAT st p ^ <*k*> in {0 ,1} * & n <= k holds
p ^ <*n*> in {0 ,1} *
let k, n be Element of 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:50;
1 in Seg 1 by FINSEQ_1:5;
then 1 in dom <*k*> by FINSEQ_1:55;
then kk . 1 in {0 ,1} by FINSEQ_2:13;
then A9: k in {0 ,1} by FINSEQ_1:57;

now

per cases ( k = 0 or k = 1 ) by A9, TARSKI:def 2;

suppose k = 0 ; :: thesis: ( n = 0 or n = 1 )

hence ( n = 0 or n = 1 ) by A7; :: thesis: verum

end;

suppose A10: k = 1 ; :: thesis: ( n = 0 or n = 1 )

( n = 1 or n = 0 )

proof

assume n <> 1 ; :: thesis: n = 0
then n < 0 + 1 by A7, A10, XXREAL_0:1;
hence n = 0 by NAT_1:13; :: thesis: verum

end;

hence ( n = 0 or n = 1 ) ; :: thesis: verum

end;

end;

end;

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:50;
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;

{0 ,1} * c= NAT * by FINSEQ_1:83;
hence {0 ,1} * is Tree by A1, A5, TREES_1:def 5; :: thesis: verum