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

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

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 } c= P ; :: according to XBOOLE_0:def 10 :: 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 } \ { 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 }

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

assume A9: 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 } \ { 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 }

A10: 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 } by Th4;

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 }

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 } by A9, A10, XBOOLE_0:def 5; :: thesis: verum

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

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

now :: thesis: for x being object st 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 } \ { 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 } holds

x in P

hence
{ 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 } holds

x in P

let x be object ; :: 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 } \ { 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 } implies x in P )

assume A1: 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 } \ { 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: x in P

then A2: 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 } ;

A3: 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 } by A1, XBOOLE_0:def 5;

assume A4: not x in P ; :: thesis: contradiction

ex t1 being Element of T st

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

not p is_a_prefix_of t1 ) )

end;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 } implies x in P )

assume A1: 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 } \ { 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: x in P

then A2: 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 } ;

A3: 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 } by A1, XBOOLE_0:def 5;

assume A4: not x in P ; :: thesis: contradiction

ex t1 being Element of T st

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

not p is_a_prefix_of t1 ) )

proof

hence
contradiction
by A3; :: thesis: verum
consider t9 being Element of T such that

A5: x = t9 and

A6: for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of t9 by A2;

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

not p is_a_prefix_of t1 ) ) by A5; :: thesis: verum

end;A5: x = t9 and

A6: for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of t9 by A2;

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

not p is_a_prefix_of t9

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

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

assume A7: p in P ; :: thesis: not b_{1} is_a_prefix_of t9

then A8: not p is_a_proper_prefix_of t9 by A6;

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

then A8: not p is_a_proper_prefix_of t9 by A6;

per cases
( not p is_a_prefix_of t9 or p = t9 )
by A8;

end;

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

not p is_a_prefix_of t1 ) ) by A5; :: thesis: verum

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 } c= P ; :: according to XBOOLE_0:def 10 :: 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 } \ { 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 }

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

assume A9: 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 } \ { 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 }

A10: 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 } by Th4;

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 }

proof

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

then ex t9 being Element of T st

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

not p is_a_prefix_of t9 ) ) ;

hence contradiction by A9; :: thesis: verum

end;not p is_a_prefix_of t1 } ; :: thesis: contradiction

then ex t9 being Element of T st

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

not p is_a_prefix_of t9 ) ) ;

hence contradiction by A9; :: thesis: verum

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 } by A9, A10, XBOOLE_0:def 5; :: thesis: verum