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 t' being Element of T such that
A1: ( x = t' & ( for p being FinSequence of NAT st p in P holds
not p is_a_prefix_of t' ) ) ;

now

let p be FinSequence of NAT ; :: thesis: ( p in P implies not p is_a_proper_prefix_of t' )
assume p in P ; :: thesis: not p is_a_proper_prefix_of t'
then not p is_a_prefix_of t' by A1;
hence not p is_a_proper_prefix_of t' 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