reconsider p9 = p as Element of T by A1;
not p is_a_proper_prefix_of p9 ;
then p in { t where t is Element of T : not p is_a_proper_prefix_of t } ;
then reconsider X = { t where t is Element of T : not p is_a_proper_prefix_of t } \/ { (p ^ s) where s is Element of T1 : verum } as non empty set ;
A2: for x being set st x in { t where t is Element of T : not p is_a_proper_prefix_of t } holds
( x is FinSequence of NAT & x in NAT * & x in T )

proof

let x be set ; :: thesis:
assume x in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis:
then A3: ex t being Element of T st
( x = t & not p is_a_proper_prefix_of t ) ;
hence x is FinSequence of NAT ; :: thesis:
thus ( x in NAT * & x in T ) by A3, FINSEQ_1:def 11; :: thesis:

end;

X is Tree-like

proof

thus X c= NAT * :: according to TREES_1:def 3 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
then A4: ( x in { t where t is Element of T : not p is_a_proper_prefix_of t } or x in { (p ^ s) where s is Element of T1 : verum } ) by XBOOLE_0:def 3;

now :: thesis:

assume x in { (p ^ s) where s is Element of T1 : verum } ; :: thesis:
then ex s being Element of T1 st x = p ^ s ;
hence x is FinSequence of NAT ; :: thesis:

end;

hence x in NAT * by A2, A4, FINSEQ_1:def 11; :: thesis:

end;

thus for q being FinSequence of NAT st q in X holds
ProperPrefixes q c= X :: thesis:

proof

let q be FinSequence of NAT ; :: thesis:
assume A5: q in X ; :: thesis:

A6: now :: thesis:

assume q in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis:
then A7: ex t being Element of T st
( q = t & not p is_a_proper_prefix_of t ) ;
then A8: ProperPrefixes q c= T by Def3;
thus ProperPrefixes q c= X :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: x in ProperPrefixes q ; :: thesis:
then consider p1 being FinSequence such that
A10: x = p1 and
A11: p1 is_a_proper_prefix_of q by Def2;
reconsider p1 = p1 as Element of T by A8, A9, A10;
not p is_a_proper_prefix_of p1 by A7, A11, XBOOLE_1:56;
then x in { s1 where s1 is Element of T : not p is_a_proper_prefix_of s1 } by A10;
hence x in X by XBOOLE_0:def 3; :: thesis:

end;

now :: thesis:

assume q in { (p ^ s) where s is Element of T1 : verum } ; :: thesis:
then consider s being Element of T1 such that
A12: q = p ^ s ;
thus ProperPrefixes q c= X :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A13: x in ProperPrefixes q ; :: thesis:
then reconsider r = x as FinSequence by Th10;
r is_a_proper_prefix_of p ^ s by A12, A13, Th11;
then r is_a_prefix_of p ^ s ;
then consider r1 being FinSequence such that
A14: p ^ s = r ^ r1 by Th1;

A15: now :: thesis:

assume len p <= len r ; :: thesis:
then consider r2 being FinSequence such that
A16: p ^ r2 = r by A14, FINSEQ_1:47;
p ^ s = p ^ (r2 ^ r1) by A14, A16, FINSEQ_1:32;
then s = r2 ^ r1 by FINSEQ_1:33;
then A17: ( dom r2 = Seg (len r2) & s | (dom r2) = r2 ) by FINSEQ_1:21, FINSEQ_1:def 3;
then reconsider r2 = r2 as FinSequence of NAT by FINSEQ_1:18;
r2 is_a_prefix_of s by A17;
then reconsider r2 = r2 as Element of T1 by Th19;
r = p ^ r2 by A16;
then r in { (p ^ v) where v is Element of T1 : verum } ;
hence r in X by XBOOLE_0:def 3; :: thesis:

end;

now :: thesis:

assume len r <= len p ; :: thesis:
then ex r2 being FinSequence st r ^ r2 = p by A14, FINSEQ_1:47;
then A18: p | (dom r) = r by FINSEQ_1:21;
A19: dom r = Seg (len r) by FINSEQ_1:def 3;
then reconsider r3 = r as FinSequence of NAT by A18, FINSEQ_1:18;
A20: r3 is_a_prefix_of p by A18, A19;
then A21: not p is_a_proper_prefix_of r3 by XBOOLE_0:def 8;
reconsider r3 = r3 as Element of T by A1, A20, Th19;
r3 in { t where t is Element of T : not p is_a_proper_prefix_of t } by A21;
hence r in X by XBOOLE_0:def 3; :: thesis:

end;

hence x in X by A15; :: thesis:

end;

hence ProperPrefixes q c= X by A5, A6, XBOOLE_0:def 3; :: thesis:

end;

let q be FinSequence of NAT ; :: thesis:
let k, n be Nat; :: thesis:
assume that
A22: q ^ <*k*> in X and
A23: n <= k ; :: thesis:

A24: now :: thesis:

assume q ^ <*k*> in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis:
then A25: ex s being Element of T st
( q ^ <*k*> = s & not p is_a_proper_prefix_of s ) ;
then reconsider u = q ^ <*n*> as Element of T by A23, Def3;

now :: thesis:

assume p is_a_proper_prefix_of u ; :: thesis:
then p is_a_prefix_of q by Th8;
hence contradiction by A25, Th7; :: thesis:

end;

then q ^ <*n*> in { t where t is Element of T : not p is_a_proper_prefix_of t } ;
hence q ^ <*n*> in X by XBOOLE_0:def 3; :: thesis:

end;

now :: thesis:

assume q ^ <*k*> in { (p ^ s) where s is Element of T1 : verum } ; :: thesis:
then consider s being Element of T1 such that
A26: q ^ <*k*> = p ^ s ;

A27: now :: thesis:

assume len q <= len p ; :: thesis:
then consider r being FinSequence such that
A28: q ^ r = p by A26, FINSEQ_1:47;
q ^ <*k*> = q ^ (r ^ s) by A26, A28, FINSEQ_1:32;
then A29: <*k*> = r ^ s by FINSEQ_1:33;

A30: now :: thesis:

assume A31: r = <*k*> ; :: thesis:
then reconsider s = q ^ <*n*> as Element of T by A1, A23, A28, Def3;

now :: thesis:

assume A32: p is_a_proper_prefix_of s ; :: thesis:
len p = (len q) + (len <*k*>) by A28, A31, FINSEQ_1:22
.= (len q) + 1 by FINSEQ_1:40
.= (len q) + (len <*n*>) by FINSEQ_1:40
.= len s by FINSEQ_1:22 ;
hence contradiction by A32, CARD_2:102; :: thesis:

end;

hence q ^ <*n*> in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis:

end;

now :: thesis:

assume that
A33: s = <*k*> and
A34: r = {} ; :: thesis:
( s = {} ^ s & {} = <*> NAT ) by FINSEQ_1:34;
then {} ^ <*n*> in T1 by A23, A33, Def3;
then reconsider t = <*n*> as Element of T1 by FINSEQ_1:34;
q ^ <*n*> = p ^ t by A28, A34, FINSEQ_1:34;
hence q ^ <*n*> in { (p ^ v) where v is Element of T1 : verum } ; :: thesis:

end;

hence q ^ <*n*> in X by A29, A30, FINSEQ_1:88, XBOOLE_0:def 3; :: thesis:

end;

now :: thesis:

assume len p <= len q ; :: thesis:
then consider r being FinSequence such that
A35: p ^ r = q by A26, FINSEQ_1:47;
p ^ (r ^ <*k*>) = p ^ s by A26, A35, FINSEQ_1:32;
then A36: r ^ <*k*> = s by FINSEQ_1:33;
then ( dom r = Seg (len r) & s | (dom r) = r ) by FINSEQ_1:21, FINSEQ_1:def 3;
then reconsider r = r as FinSequence of NAT by FINSEQ_1:18;
reconsider t = r ^ <*n*> as Element of T1 by A23, A36, Def3;
q ^ <*n*> = p ^ t by A35, FINSEQ_1:32;
then q ^ <*n*> in { (p ^ v) where v is Element of T1 : verum } ;
hence q ^ <*n*> in X by XBOOLE_0:def 3; :: thesis:

end;

hence q ^ <*n*> in X by A27; :: thesis:

end;

hence q ^ <*n*> in X by A22, A24, XBOOLE_0:def 3; :: thesis:

end;

then reconsider X = X as Tree ;
take X ; :: thesis:
let q be FinSequence of NAT ; :: thesis:
thus ( not q in X or ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) :: thesis:

proof

assume A37: q in X ; :: thesis:

A38: now :: thesis:

assume q in { t where t is Element of T : not p is_a_proper_prefix_of t } ; :: thesis:
then ex s being Element of T st
( q = s & not p is_a_proper_prefix_of s ) ;
hence ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ; :: thesis:

end;

now :: thesis:

assume q in { (p ^ s) where s is Element of T1 : verum } ; :: thesis:
then ex s being Element of T1 st q = p ^ s ;
hence ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ; :: thesis:

end;

hence ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) by A37, A38, XBOOLE_0:def 3; :: thesis:

end;

assume A39: ( ( q in T & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) ; :: thesis:
A40: ( q in T & not p is_a_proper_prefix_of q implies q in { t where t is Element of T : not p is_a_proper_prefix_of t } ) ;
( ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) implies q in { (p ^ v) where v is Element of T1 : verum } ) ;
hence q in X by A39, A40, XBOOLE_0:def 3; :: thesis: