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 object ; :: 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
A1: r1 in C and
A2: 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
A3: r2 in C and
A4: q is_a_prefix_of r2 ;
r1,r2 are_c=-comparable by A1, A3, Def3;
then ( r1 is_a_prefix_of r2 or r2 is_a_prefix_of r1 ) ;
then ( p is_a_prefix_of r2 or q is_a_prefix_of r1 ) by A2, A4;
hence p,q are_c=-comparable by A2, A4, 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