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 object ; :: 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 }
then reconsider q = x as FinSequence of NAT by TREES_1:19;

A3: now :: thesis: ( ex p, r being FinSequence of NAT st
( p in P & r in T1 & q = p ^ r ) implies x in { (p9 ^ s) where p9 is Element of T, s is Element of T1 : p9 in P } )

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 }
P c= T by TREES_1:def 11;
hence x in { (p9 ^ s) where p9 is Element of T, s is Element of T1 : p9 in P } by A4; :: thesis: verum

end;

( 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 } ) ;
hence 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, Def1, XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: 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 A5: 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)

A6: now :: thesis: ( x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } implies x in tree (T,P,T1) )

assume 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)
then ex p being Element of T ex s being Element of T1 st
( x = p ^ s & p in P ) ;
hence x in tree (T,P,T1) by Def1; :: thesis: verum

end;

now :: 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 } implies x in tree (T,P,T1) )

assume 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)
then 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 ) ) ;
hence x in tree (T,P,T1) by A1, Def1; :: thesis: verum

end;

hence x in tree (T,P,T1) by A5, A6, XBOOLE_0:def 3; :: thesis: verum