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_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_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_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P }
then A2: 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 } by Th2;
thus tree (T,P,T1) c= { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } \/ { (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_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 { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )
assume x in tree (T,P,T1) ; :: thesis: x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P }
then A3: 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 } by A1, Th2;

now :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

per cases ( x in P or not x in P ) ;

suppose A4: x in P ; :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

P c= { (p ^ s) where p is Element of T, s is Element of T1 : p in P } by Th6;
hence ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ) by A4; :: thesis: verum

end;

suppose A5: not x in P ; :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

now :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

per cases ( 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 } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ) by A3, XBOOLE_0:def 3;

suppose A6: 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 } ; :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 }

proof

assume A7: 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_prefix_of t1 } ; :: thesis: contradiction
{ 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 } \ { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } = P by Th5;
hence contradiction by A5, A6, A7, XBOOLE_0:def 5; :: thesis: verum

end;

hence ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ) ; :: thesis: verum

end;

suppose x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ; :: thesis: ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } )

hence ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ) ; :: thesis: verum

end;

end;

end;

hence ( x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } or x in { (p ^ s) where p is Element of T, s is Element of T1 : p in P } ) ; :: thesis: verum

end;

end;

end;

hence x in { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } by XBOOLE_0:def 3; :: thesis: verum

end;

thus { t1 where t1 is Element of T : for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t1 } \/ { (p ^ s) where p is Element of T, s is Element of T1 : p in P } c= tree (T,P,T1) by A2, Th3, XBOOLE_1:9; :: thesis: verum