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();
A18: ( <*> 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;
reconsider X = X as non empty set by A17, A18;
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 A22: x in ProperPrefixes q ; :: thesis: x in X
consider r being FinSequence such that
A23: x = r and
A24: r is_a_proper_prefix_of q by A22, Def4;
A25: r is_a_prefix_of q by A24, XBOOLE_0:def 8;
A26: ex n being Element of NAT st r = q | (Seg n) by A25, Def1;
reconsider r = r as FinSequence of NAT by A26, 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;
A29: p ^ q = (p ^ r) ^ s by A27, FINSEQ_1:45;
A30: ( r in NAT * & ( for q being FinSequence of NAT st r = q holds
p ^ q in T ) ) by A28, A29, Th46, FINSEQ_1:def 11;
thus x in X by A17, A23, A30; :: thesis: verum

end;

end;

A31: 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
A34: p ^ (q ^ <*k*>) in T by A17, A32;
A35: (p ^ q) ^ <*k*> in T by A34, FINSEQ_1:45;
A36: (p ^ q) ^ <*n*> in T by A33, A35, Def5;
A37: ( q ^ <*n*> in NAT * & ( for r being FinSequence of NAT st r = q ^ <*n*> holds
p ^ r in T ) ) by A36, FINSEQ_1:45, FINSEQ_1:def 11;
thus q ^ <*n*> in X by A17, A37; :: thesis: verum

end;

reconsider X = X as Tree by A19, A20, A31, 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 A38: p ^ q in T ; :: thesis: q in X
A39: ( q in NAT * & ( for r being FinSequence of NAT st q = r holds
p ^ r in T ) ) by A38, FINSEQ_1:def 11;
thus q in X by A17, A39; :: thesis: verum