defpred S₁[ set ] means for q being FinSequence of NAT st $1 = q holds
p ^ q in T;
consider X being set such that
A11: for x being set holds
( x in X iff ( x in NAT * & S₁[x] ) ) from XBOOLE_0:sch 1();
( <*> NAT in NAT * & ( for q being FinSequence of NAT st <*> NAT = q holds
p ^ q in T ) ) by B11, FINSEQ_1:34, FINSEQ_1:def 11;
then reconsider X = X as non empty set by A11;
A12: X c= NAT *

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in NAT * )
thus ( not x in X or x in NAT * ) by A11; :: thesis: verum

end;

A13: now :: thesis: for q being FinSequence of NAT st q in X holds
ProperPrefixes q c= X

let q be FinSequence of NAT ; :: thesis: ( q in X implies ProperPrefixes q c= X )
assume A14: q in X ; :: thesis: ProperPrefixes q c= X
thus ProperPrefixes q c= X :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes q or x in X )
assume x in ProperPrefixes q ; :: thesis: x in X
then consider r being FinSequence such that
A15: x = r and
A16: r is_a_proper_prefix_of q by Def2;
r is_a_prefix_of q by A16, XBOOLE_0:def 8;
then A17: ex n being Element of NAT st r = q | (Seg n) by Def1;
then reconsider r = r as FinSequence of NAT by FINSEQ_1:18;
consider s being FinSequence such that
A18: q = r ^ s by A17, FINSEQ_1:80;
A19: p ^ q in T by A11, A14;
p ^ q = (p ^ r) ^ s by A18, FINSEQ_1:32;
then ( r in NAT * & ( for q being FinSequence of NAT st r = q holds
p ^ q in T ) ) by A19, Th21, FINSEQ_1:def 11;
hence x in X by A11, A15; :: thesis: verum

end;

end;

now :: thesis: for q being FinSequence of NAT
for k, n being Element of NAT st q ^ <*k*> in X & n <= k holds
q ^ <*n*> in X

let q be FinSequence of NAT ; :: thesis: for k, n being Element of NAT st q ^ <*k*> in X & n <= k holds
q ^ <*n*> in X
let k, n be Element of NAT ; :: thesis: ( q ^ <*k*> in X & n <= k implies q ^ <*n*> in X )
assume that
A20: q ^ <*k*> in X and
A21: n <= k ; :: thesis: q ^ <*n*> in X
p ^ (q ^ <*k*>) in T by A11, A20;
then (p ^ q) ^ <*k*> in T by FINSEQ_1:32;
then (p ^ q) ^ <*n*> in T by A21, Def3;
then ( q ^ <*n*> in NAT * & ( for r being FinSequence of NAT st r = q ^ <*n*> holds
p ^ r in T ) ) by FINSEQ_1:32, FINSEQ_1:def 11;
hence q ^ <*n*> in X by A11; :: thesis: verum

end;

then reconsider X = X as Tree by A12, A13, Def3;
take X ; :: thesis: for q being FinSequence of NAT holds
( q in X iff p ^ q in T )
let q be FinSequence of NAT ; :: thesis: ( q in X iff p ^ q in T )
thus ( q in X implies p ^ q in T ) by A11; :: thesis: ( p ^ q in T implies q in X )
assume p ^ q in T ; :: thesis: q in X
then ( q in NAT * & ( for r being FinSequence of NAT st q = r holds
p ^ r in T ) ) by FINSEQ_1:def 11;
hence q in X by A11; :: thesis: verum