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 }
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 A1, 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 set ; :: 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 A3: 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 }
A4: 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, A3, Th2;

A5: now

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

suppose A6: 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 } )

A7: P c= { (p ^ s) where p is Element of T, s is Element of T1 : p in P } by Th6;
thus ( 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 A6, A7; :: thesis: verum

end;

suppose A8: 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 } )

A9: now

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 A4, XBOOLE_0:def 3;

suppose A10: 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 } )

A11: 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 A12: 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
A13: { 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;
thus contradiction by A8, A10, A12, A13, XBOOLE_0:def 5; :: thesis: verum

end;

thus ( 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 A11; :: thesis: verum

end;

suppose A14: 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 } )

thus ( 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 A14; :: thesis: verum

end;

end;

end;

thus ( 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 A9; :: thesis: verum

end;

end;

end;

thus 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 A5, 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