defpred S₁[ set ] means for q being FinSequence of NAT st $1 = q holds
p ^ q in T;
consider X being set such that
A9: 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 A8, FINSEQ_1:47, FINSEQ_1:def 11;
then reconsider X = X as non empty set by A9;
A10: 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 A9; :: thesis: verum

end;

A11: now

let q be FinSequence of NAT ; :: thesis: ( q in X implies ProperPrefixes q c= X )
assume A12: 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
A13: ( x = r & r is_a_proper_prefix_of q ) by Def4;
r is_a_prefix_of q by A13, XBOOLE_0:def 8;
then A14: ex n being Element of NAT st r = q | (Seg n) by Def1;
then reconsider r = r as FinSequence of NAT by FINSEQ_1:23;
consider s being FinSequence such that
A15: q = r ^ s by A14, FINSEQ_1:101;
( p ^ q in T & p ^ q = (p ^ r) ^ s ) by A9, A12, A15, FINSEQ_1:45;
then ( r in NAT * & ( for q being FinSequence of NAT st r = q holds
p ^ q in T ) ) by Th46, FINSEQ_1:def 11;
hence x in X by A9, A13; :: thesis: verum

end;

end;

now

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 A16: ( q ^ <*k*> in X & n <= k ) ; :: thesis: q ^ <*n*> in X
then p ^ (q ^ <*k*>) in T by A9;
then (p ^ q) ^ <*k*> in T by FINSEQ_1:45;
then (p ^ q) ^ <*n*> in T by A16, Def5;
then ( q ^ <*n*> in NAT * & ( for r being FinSequence of NAT st r = q ^ <*n*> holds
p ^ r in T ) ) by FINSEQ_1:45, FINSEQ_1:def 11;
hence q ^ <*n*> in X by A9; :: thesis: verum

end;

then reconsider X = X as Tree by A10, A11, Def5;
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 A9; :: 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 A9; :: thesis: verum