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