let T be Tree; :: thesis: for P being AntiChain_of_Prefixes of T holds P c= { 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 }

let P be AntiChain_of_Prefixes of T; :: thesis: P c= { 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 }

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P 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_proper_prefix_of t1 } )

assume A1: 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_proper_prefix_of t1 }

ex t1 being Element of T st

( x = t1 & ( for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of t1 ) )

not p is_a_proper_prefix_of t1 } ; :: thesis: verum

not p is_a_proper_prefix_of t1 }

let P be AntiChain_of_Prefixes of T; :: thesis: P c= { 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 }

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P 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_proper_prefix_of t1 } )

assume A1: 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_proper_prefix_of t1 }

ex t1 being Element of T st

( x = t1 & ( for p being FinSequence of NAT st p in P holds

not p is_a_proper_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
P c= T
by TREES_1:def 11;

then consider t9 being Element of T such that

A2: t9 = x by A1;

( x = t1 & ( for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of t1 ) ) by A2; :: thesis: verum

end;then consider t9 being Element of T such that

A2: t9 = x by A1;

now :: thesis: for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of t9

hence
ex t1 being Element of T st not p is_a_proper_prefix_of t9

let p be FinSequence of NAT ; :: thesis: ( p in P implies not b_{1} is_a_proper_prefix_of t9 )

assume A3: p in P ; :: thesis: not b_{1} is_a_proper_prefix_of t9

end;assume A3: p in P ; :: thesis: not b

per cases
( t9 = p or t9 <> p )
;

end;

suppose
t9 <> p
; :: thesis: not b_{1} is_a_proper_prefix_of t9

then
not t9,p are_c=-comparable
by A1, A2, A3, TREES_1:def 10;

hence not p is_a_proper_prefix_of t9 ; :: thesis: verum

end;hence not p is_a_proper_prefix_of t9 ; :: thesis: verum

( x = t1 & ( for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of t1 ) ) by A2; :: thesis: verum

not p is_a_proper_prefix_of t1 } ; :: thesis: verum