let W be Tree; :: thesis: for C being Chain of W holds { w where w is Element of W : ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) } is Chain of W
let C be Chain of W; :: thesis: { w where w is Element of W : ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) } is Chain of W
{ w where w is Element of W : ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) } c= W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { w where w is Element of W : ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) } or x in W )
assume x in { w where w is Element of W : ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) } ; :: thesis: x in W
then ex w being Element of W st
( x = w & ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) ) ;
hence x in W ; :: thesis: verum

end;

then reconsider Z = { w where w is Element of W : ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) } as Subset of W ;
Z is Chain of W

proof

let p be FinSequence of NAT ; :: according to TREES_2:def 3 :: thesis: for q being FinSequence of NAT st p in Z & q in Z holds
p,q are_c=-comparable
let q be FinSequence of NAT ; :: thesis: ( p in Z & q in Z implies p,q are_c=-comparable )
assume p in Z ; :: thesis: ( not q in Z or p,q are_c=-comparable )
then ex w being Element of W st
( p = w & ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) ) ;
then consider r1 being FinSequence of NAT such that
A7: r1 in C and
A8: p is_a_prefix_of r1 ;
assume q in Z ; :: thesis: p,q are_c=-comparable
then ex w9 being Element of W st
( q = w9 & ex p being FinSequence of NAT st
( p in C & w9 is_a_prefix_of p ) ) ;
then consider r2 being FinSequence of NAT such that
A11: r2 in C and
A12: q is_a_prefix_of r2 ;
r1,r2 are_c=-comparable by A7, A11, Def3;
then ( r1 is_a_prefix_of r2 or r2 is_a_prefix_of r1 ) by XBOOLE_0:def 9;
then ( p is_a_prefix_of r2 or q is_a_prefix_of r1 ) by A8, A12, XBOOLE_1:1;
hence p,q are_c=-comparable by A8, A12, Th1; :: thesis: verum

end;

hence { w where w is Element of W : ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) } is Chain of W ; :: thesis: verum