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

end;

A20: now

let q be FinSequence of NAT ; :: thesis: ( q in X implies ProperPrefixes q c= X )
assume A21: 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
A23: x = r and
A24: r is_a_proper_prefix_of q by Def4;
r is_a_prefix_of q by A24, XBOOLE_0:def 8;
then A26: 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
A27: q = r ^ s by A26, FINSEQ_1:101;
A28: p ^ q in T by A17, A21;
p ^ q = (p ^ r) ^ s by A27, FINSEQ_1:45;
then ( r in NAT * & ( for q being FinSequence of NAT st r = q holds
p ^ q in T ) ) by A28, Th46, FINSEQ_1:def 11;
hence x in X by A17, A23; :: 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 that
A32: q ^ <*k*> in X and
A33: n <= k ; :: thesis: q ^ <*n*> in X
p ^ (q ^ <*k*>) in T by A17, A32;
then (p ^ q) ^ <*k*> in T by FINSEQ_1:45;
then (p ^ q) ^ <*n*> in T by A33, 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 A17; :: thesis: verum

end;

then reconsider X = X as Tree by A19, A20, 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 A17; :: 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 A17; :: thesis: verum