let T, T1 be Tree; :: thesis:
let P be AntiChain_of_Prefixes of T; :: thesis:
let p be FinSequence of NAT ; :: thesis:
assume A1: p in P ; :: thesis:
ex q, r being FinSequence of NAT st
( q in P & r in T1 & p = q ^ r )

proof

consider q being FinSequence of NAT such that
A2: q = p ;
consider r being FinSequence of NAT such that
A3: r = <*> NAT ;
A4: r in T1 by A3, TREES_1:22;
p = q ^ r by A2, A3, FINSEQ_1:34;
hence ex q, r being FinSequence of NAT st
( q in P & r in T1 & p = q ^ r ) by A1, A2, A4; :: thesis:

end;

then A5: p in tree (T,P,T1) by Def1;
let x be FinSequence of NAT ; :: according to TREES_2:def 1 :: thesis:
thus ( x in T1 implies x in (tree (T,P,T1)) | p ) :: thesis:

proof

assume x in T1 ; :: thesis:
then p ^ x in tree (T,P,T1) by A1, Def1;
hence x in (tree (T,P,T1)) | p by A5, TREES_1:def 6; :: thesis:

end;

thus ( x in (tree (T,P,T1)) | p implies x in T1 ) :: thesis:

proof

assume x in (tree (T,P,T1)) | p ; :: thesis:
then A6: p ^ x in tree (T,P,T1) by A5, TREES_1:def 6;

A7: now :: thesis:

assume that
p ^ x in T and
A8: for r being FinSequence of NAT st r in P holds
not r is_a_proper_prefix_of p ^ x ; :: thesis:
A9: not p is_a_proper_prefix_of p ^ x by A1, A8;
p is_a_prefix_of p ^ x by TREES_1:1;
then p ^ x = p by A9
.= p ^ (<*> NAT) by FINSEQ_1:34 ;
then x = {} by FINSEQ_1:33;
hence x in T1 by TREES_1:22; :: thesis:

end;

now :: thesis:

given s, r being FinSequence of NAT such that A10: s in P and
A11: r in T1 and
A12: p ^ x = s ^ r ; :: thesis:

now :: thesis:

assume s <> p ; :: thesis:
then not s,p are_c=-comparable by A1, A10, TREES_1:def 10;
hence contradiction by A12, Th1; :: thesis:

end;

hence x in T1 by A11, A12, FINSEQ_1:33; :: thesis:

end;

hence x in T1 by A1, A6, A7, Def1; :: thesis:

end;