let T be Tree; :: thesis: for P being AntiChain_of_Prefixes of T holds 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 }
let P be AntiChain_of_Prefixes of T; :: 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 }
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 } )
assume A1: 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 }
ex t1 being Element of T st
( x = t1 & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 ) )

proof

P c= T by TREES_1:def 14;
then consider t9 being Element of T such that
A4: t9 = x by A1;

now

let p be FinSequence of NAT ; :: thesis: ( p in P implies not b₁ is_a_proper_prefix_of t9 )
assume A6: p in P ; :: thesis: not b₁ is_a_proper_prefix_of t9

per cases ( t9 = p or t9 <> p ) ;

suppose t9 = p ; :: thesis: not b₁ is_a_proper_prefix_of t9

hence not p is_a_proper_prefix_of t9 ; :: thesis: verum

end;

suppose t9 <> p ; :: thesis: not b₁ is_a_proper_prefix_of t9

then not t9,p are_c=-comparable by A1, A4, A6, TREES_1:def 13;
hence not p is_a_proper_prefix_of t9 by XBOOLE_1:104; :: thesis: verum

end;

end;

end;

hence ex t1 being Element of T st
( x = t1 & ( for p being FinSequence of NAT st p in P holds
not p is_a_proper_prefix_of t1 ) ) by A4; :: 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 } ; :: thesis: verum