set X = {0 ,1} * ;
A1: {0 ,1} * c= NAT * by FINSEQ_1:83;

A2: now

let p be FinSequence of NAT ; :: thesis: ( p in {0 ,1} * implies ProperPrefixes p c= {0 ,1} * )
assume A3: 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
A4: y = q and
A5: q is_a_proper_prefix_of p by TREES_1:def 4;
q is_a_prefix_of p by A5, XBOOLE_0:def 8;
then consider n being Element of NAT such that
A6: q = p | (Seg n) by TREES_1:def 1;
thus y in {0 ,1} * by A3, A4, A6, Th1; :: thesis: verum

end;

end;

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
A7: p ^ <*k*> in {0 ,1} * and
A8: n <= k ; :: thesis: p ^ <*n*> in {0 ,1} *
A9: p ^ <*k*> is FinSequence of {0 ,1} by A7, FINSEQ_1:def 11;
then A10: ( p is FinSequence of {0 ,1} & <*k*> is FinSequence of {0 ,1} ) by FINSEQ_1:50;
reconsider kk = <*k*> as FinSequence of {0 ,1} by A9, 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 A11: k in {0 ,1} by FINSEQ_1:57;

now

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

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

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

end;

suppose A12: 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 A8, A12, XXREAL_0:1;
then n <= 0 by NAT_1:13;
hence n = 0 ; :: thesis: verum

end;

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

end;

end;

end;

then n in {0 ,1} by TARSKI:def 2;
then <*n*> is FinSequence of {0 ,1} by Lm2;
then p ^ <*n*> is FinSequence of {0 ,1} by A10, Lm1;
hence p ^ <*n*> in {0 ,1} * by FINSEQ_1:def 11; :: thesis: verum

end;

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