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)

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

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

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

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

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

end;

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

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

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

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;

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

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;

end;

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

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 }

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;not p is_a_prefix_of t1 }

proof

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

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

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

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

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

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

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