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)

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)

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 { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
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;

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;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 } )

( q in T & ( for p being FinSequence of NAT st p in P holds ( 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;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

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

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;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

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) )

hence
x in tree (T,P,T1)
by A5, A6, XBOOLE_0:def 3; :: thesis: verumnot 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;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