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

A1: now

let x be set ; :: 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 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 } \ { 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
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 } by A2;
A4: 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 A2, XBOOLE_0:def 5;
assume A5: not x in P ; :: thesis: contradiction
A6: 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

consider t9 being Element of T such that
A7: x = t9 and
A8: for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t9 by A3;

A9: now

let p be FinSequence of NAT ; :: thesis: ( p in P implies not b₁ is_a_prefix_of t9 )
assume A10: p in P ; :: thesis: not b₁ is_a_prefix_of t9
A11: not p is_a_proper_prefix_of t9 by A8, A10;

per cases ( not p is_a_prefix_of t9 or p = t9 ) by A11, XBOOLE_0:def 8;

suppose A12: not p is_a_prefix_of t9 ; :: thesis: not b₁ is_a_prefix_of t9

thus not p is_a_prefix_of t9 by A12; :: thesis: verum

end;

suppose A13: p = t9 ; :: thesis: not b₁ is_a_prefix_of t9

thus not p is_a_prefix_of t9 by A5, A7, A10, A13; :: thesis: verum

end;

end;

end;

thus 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 ) ) by A7, A9; :: thesis: verum

end;

thus contradiction by A4, A6; :: 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_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 by A1, TARSKI:def 3; :: 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 set ; :: 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 A14: 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 }
A15: 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;
A16: 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

assume A17: 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
A18: 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 ) ) by A17;
thus contradiction by A14, A18; :: 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_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 A14, A15, A16, XBOOLE_0:def 5; :: thesis: verum