set X = {0,1} * ;

A1: now :: thesis: for p being FinSequence of NAT st p in {0,1} * holds
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

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;

end;

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} *

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} ;

now :: thesis: ( n = 0 or n = 1 )

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

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