defpred S1[ object ] means for q being FinSequence of NAT st $1 = q holds
p ^ q in T;
consider X being set such that
A12: for x being object holds
( x in X iff ( x in NAT * & S1[x] ) ) from XBOOLE_0:sch 1();
 ( <*> NAT in NAT * & ( for q being FinSequence of NAT st <*> NAT = q holds
p ^ q in T ) ) by A11, FINSEQ_1:34, FINSEQ_1:def 11;
then reconsider X = X as non empty set by A12;
A13: X c= NAT * by A12;
A14: 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 A15: q in X ; :: thesis: ProperPrefixes q c= X
thus ProperPrefixes q c= X :: thesis: verum
proof
let x be object ; :: 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
A16: x = r and
A17: r is_a_proper_prefix_of q by Def2;
r is_a_prefix_of q by A17;
then A18: ex n being Nat st r = q | (Seg n) ;
then reconsider r = r as FinSequence of NAT by FINSEQ_1:18;
consider s being FinSequence such that
A19: q = r ^ s by A18, FINSEQ_1:80;
A20: p ^ q in T by A12, A15;
p ^ q = (p ^ r) ^ s by A19, FINSEQ_1:32;
then ( r in NAT * & ( for q being FinSequence of NAT st r = q holds
p ^ q in T ) ) by A20, Th20, FINSEQ_1:def 11;
hence x in X by A12, A16; :: thesis: verum
end;
end;
now :: thesis: for q being FinSequence of NAT
for k, n being Nat st q ^ <*k*> in X & n <= k holds
q ^ <*n*> in X
let q be FinSequence of NAT ; :: thesis: for k, n being Nat st q ^ <*k*> in X & n <= k holds
q ^ <*n*> in X
let k, n be Nat; :: thesis: ( q ^ <*k*> in X & n <= k implies q ^ <*n*> in X )
assume that
A21: q ^ <*k*> in X and
A22: n <= k ; :: thesis: q ^ <*n*> in X
reconsider kk = k, nn = n as Element of NAT by ORDINAL1:def 12;
p ^ (q ^ <*kk*>) in T by A12, A21;
then (p ^ q) ^ <*k*> in T by FINSEQ_1:32;
then (p ^ q) ^ <*n*> in T by A22, Def3;
then ( q ^ <*nn*> in NAT * & ( for r being FinSequence of NAT st r = q ^ <*nn*> holds
p ^ r in T ) ) by FINSEQ_1:32, FINSEQ_1:def 11;
hence q ^ <*n*> in X by A12; :: thesis: verum
end;
then reconsider X = X as Tree by A13, A14, 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 A12; :: 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 A12; :: thesis: verum