defpred S1[ object ] means ( \$1 in F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & \$1 = q ^ r ) );
consider T being set such that
A1: for x being object holds
( x in T iff ( x in NAT * & S1[x] ) ) from set t = the Element of F1();
the Element of F1() in NAT * by FINSEQ_1:def 11;
then reconsider T = T as non empty set by A1;
T is Tree-like
proof
thus T c= NAT * by A1; :: according to TREES_1:def 3 :: thesis: ( ( for b1 being FinSequence of NAT holds
( not b1 in T or ProperPrefixes b1 c= T ) ) & ( for b1 being FinSequence of NAT
for b2, b3 being set holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T ) ) )

thus for p being FinSequence of NAT st p in T holds
ProperPrefixes p c= T :: thesis: for b1 being FinSequence of NAT
for b2, b3 being set holds
( not b1 ^ <*b2*> in T or not b3 <= b2 or b1 ^ <*b3*> in T )
proof
let p be FinSequence of NAT ; :: thesis: ( p in T implies ProperPrefixes p c= T )
assume A2: p in T ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes p or x in T )
assume x in ProperPrefixes p ; :: thesis: x in T
then consider q being FinSequence such that
A3: x = q and
A4: q is_a_proper_prefix_of p by TREES_1:def 2;
assume A5: not x in T ; :: thesis: contradiction
q is_a_prefix_of p by ;
then consider r being FinSequence such that
A6: p = q ^ r by TREES_1:1;
reconsider q = q, r = r as FinSequence of NAT by ;
( ( q ^ r in F1() & q in NAT * & ( q ^ r in F1() implies q in F1() ) ) or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & p = q ^ r ) ) by ;
then consider q9 being Element of F1(), r9 being Element of F2() such that
A7: P1[q9] and
A8: q ^ r = q9 ^ r9 by A1, A3, A5, A6;
then consider s being FinSequence such that
A10: q9 ^ s = q by ;
reconsider s = s as FinSequence of NAT by ;
q9 ^ r9 = q9 ^ (s ^ r) by ;
then s ^ r = r9 by FINSEQ_1:33;
then ( q in NAT * & s is Element of F2() ) by ;
hence contradiction by A1, A3, A5, A7, A10; :: thesis: verum
end;
let p be FinSequence of NAT ; :: thesis: for b1, b2 being set holds
( not p ^ <*b1*> in T or not b2 <= b1 or p ^ <*b2*> in T )

let k, n be Nat; :: thesis: ( not p ^ <*k*> in T or not n <= k or p ^ <*n*> in T )
assume that
A11: p ^ <*k*> in T and
A12: n <= k ; :: thesis: p ^ <*n*> in T
A13: now :: thesis: ( p ^ <*k*> in F1() implies p ^ <*n*> in T )
assume p ^ <*k*> in F1() ; :: thesis: p ^ <*n*> in T
then A14: p ^ <*n*> in F1() by ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
p ^ <*n*> in NAT * by FINSEQ_1:def 11;
hence p ^ <*n*> in T by ; :: thesis: verum
end;
now :: thesis: ( not p ^ <*k*> in F1() implies p ^ <*n*> in T )
assume A15: not p ^ <*k*> in F1() ; :: thesis: p ^ <*n*> in T
then consider q being Element of F1(), r being Element of F2() such that
A16: P1[q] and
A17: p ^ <*k*> = q ^ r by ;
q ^ {} = q by FINSEQ_1:34;
then r <> {} by ;
then consider w being FinSequence, z being object such that
A18: r = w ^ <*z*> by FINSEQ_1:46;
reconsider w = w as FinSequence of NAT by ;
A19: p ^ <*k*> = (q ^ w) ^ <*z*> by ;
A20: ( (p ^ <*k*>) . ((len p) + 1) = k & ((q ^ w) ^ <*z*>) . ((len (q ^ w)) + 1) = z ) by FINSEQ_1:42;
A21: ( len <*k*> = 1 & len <*z*> = 1 ) by FINSEQ_1:40;
A22: ( len (p ^ <*k*>) = (len p) + () & len ((q ^ w) ^ <*z*>) = (len (q ^ w)) + () ) by FINSEQ_1:22;
then A23: p = q ^ w by ;
A24: w ^ <*n*> in F2() by ;
A25: p ^ <*n*> = q ^ (w ^ <*n*>) by ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
p ^ <*n*> in NAT * by FINSEQ_1:def 11;
hence p ^ <*n*> in T by A1, A16, A24, A25; :: thesis: verum
end;
hence p ^ <*n*> in T by A13; :: thesis: verum
end;
then reconsider T = T as Tree ;
take T ; :: thesis: for p being FinSequence holds
( p in T iff ( p in F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & p = q ^ r ) ) )

let p be FinSequence; :: thesis: ( p in T iff ( p in F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & p = q ^ r ) ) )

( ( p is Element of F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & p = q ^ r ) ) implies p in NAT * ) by FINSEQ_1:def 11;
hence ( p in T iff ( p in F1() or ex q being Element of F1() ex r being Element of F2() st
( P1[q] & p = q ^ r ) ) ) by A1; :: thesis: verum