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 object ; :: 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 ;

for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of t9 by A2;

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

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 object ; :: 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 ;

for p being FinSequence of NAT st p in P holds

not p is_a_proper_prefix_of t9 by A2;

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