let T, T1 be Tree; :: thesis: for P being AntiChain_of_Prefixes of T st P <> {} holds
tree T,P,T1 = { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P }
let P be AntiChain_of_Prefixes of T; :: thesis: ( P <> {} implies tree T,P,T1 = { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )
assume A1: P <> {} ; :: thesis: tree T,P,T1 = { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P }
thus tree T,P,T1 c= { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } :: according to XBOOLE_0:def 10 :: thesis: { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } c= tree T,P,T1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in tree T,P,T1 or x in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )
assume A2: x in tree T,P,T1 ; :: thesis: x in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P }
reconsider q = x as FinSequence of NAT by A2, TREES_1:44;

A3: now

given p, r being FinSequence of NAT such that A4: ( p in P & r in T1 & q = p ^ r ) ; :: thesis: x in { (p9 ^ s) where p9 is Element of T, s is Element of T1 : p9 in P }
A5: P c= T by TREES_1:def 14;
thus x in { (p9 ^ s) where p9 is Element of T, s is Element of T1 : p9 in P } by A4, A5; :: thesis: verum

end;

A6: ( q in T & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of q ) implies x in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } ) ;
thus x in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } by A1, A2, A3, A6, Def1, XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } or x in tree T,P,T1 )
assume A7: x in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ; :: thesis: x in tree T,P,T1

A8: now

assume A9: x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ; :: thesis: x in tree T,P,T1
A10: ex p being Element of T ex s being Element of T1 st
( x = p ^ s & p in P ) by A9;
thus x in tree T,P,T1 by A10, Def1; :: thesis: verum

end;

A11: now

assume A12: x in { t where t is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t } ; :: thesis: x in tree T,P,T1
A13: ex t being Element of T st
( x = t & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t ) ) by A12;
thus x in tree T,P,T1 by A1, A13, Def1; :: thesis: verum

end;

thus x in tree T,P,T1 by A7, A8, A11, XBOOLE_0:def 3; :: thesis: verum