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_prefix_of t1 } 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: { 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= { 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 set ; :: according to TARSKI:def 3 :: thesis: ( 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 } 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 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: 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 }
then consider t9 being Element of T such that
A1: x = t9 and
A2: for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t9 ;

now

let p be FinSequence of NAT ; :: thesis: ( p in P implies not p is_a_proper_prefix_of t9 )
assume p in P ; :: thesis: not p is_a_proper_prefix_of t9
then not p is_a_prefix_of t9 by A2;
hence not p is_a_proper_prefix_of t9 by XBOOLE_0:def 8; :: 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_proper_prefix_of t1 } by A1; :: thesis: verum