let T1, T be Tree; :: thesis: for P being AntiChain_of_Prefixes of T
for p being FinSequence of NAT st p in P holds
T1 = (tree T,P,T1) | p
let P be AntiChain_of_Prefixes of T; :: thesis: for p being FinSequence of NAT st p in P holds
T1 = (tree T,P,T1) | p
let p be FinSequence of NAT ; :: thesis: ( p in P implies T1 = (tree T,P,T1) | p )
assume A1: p in P ; :: thesis: T1 = (tree T,P,T1) | p
A2: 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
A3: q = p ;
consider r being FinSequence of NAT such that
A4: r = <*> NAT ;
A5: r in T1 by A4, TREES_1:47;
A6: p = q ^ r by A3, A4, FINSEQ_1:47;
thus ex q, r being FinSequence of NAT st
( q in P & r in T1 & p = q ^ r ) by A1, A3, A5, A6; :: thesis: verum

end;

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

proof

assume A8: x in T1 ; :: thesis: x in (tree T,P,T1) | p
A9: p ^ x in tree T,P,T1 by A1, A8, Def1;
thus x in (tree T,P,T1) | p by A7, A9, TREES_1:def 9; :: thesis: verum

end;

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

proof

assume A10: x in (tree T,P,T1) | p ; :: thesis: x in T1
A11: p ^ x in tree T,P,T1 by A7, A10, TREES_1:def 9;

A12: now

assume that
p ^ x in T and
A13: for r being FinSequence of NAT st r in P holds
not r is_a_proper_prefix_of p ^ x ; :: thesis: x in T1
A14: not p is_a_proper_prefix_of p ^ x by A1, A13;
A15: p is_a_prefix_of p ^ x by TREES_1:8;
A16: p ^ x = p by A14, A15, XBOOLE_0:def 8
.= p ^ (<*> NAT ) by FINSEQ_1:47 ;
A17: x = {} by A16, FINSEQ_1:46;
thus x in T1 by A17, TREES_1:47; :: thesis: verum

end;

A18: now

given s, r being FinSequence of NAT such that A19: s in P and
A20: r in T1 and
A21: p ^ x = s ^ r ; :: thesis: x in T1

A22: now

assume A23: s <> p ; :: thesis: contradiction
A24: not s,p are_c=-comparable by A1, A19, A23, TREES_1:def 13;
thus contradiction by A21, A24, Th1; :: thesis: verum

end;

thus x in T1 by A20, A21, A22, FINSEQ_1:46; :: thesis: verum

end;

thus x in T1 by A1, A11, A12, A18, Def1; :: thesis: verum

end;