let W be Tree; :: thesis:
let C be Chain of W; :: thesis:
defpred S₁[ set ] means ( $1 is Chain of W & C c= $1 & ( for p being FinSequence of NAT st p in $1 holds
ProperPrefixes p c= $1 ) );
consider X being set such that
A1: for Y being set holds
( Y in X iff ( Y in bool W & S₁[Y] ) ) from XFAMILY:sch 1();
set Z = { w where w is Element of W : ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) } ;
A2: { 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 by Th24;
A3: C c= { w where w is Element of W : ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) }

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A4: x in C ; :: thesis:
then reconsider w = x as Element of W ;
w is_a_prefix_of w ;
hence 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 ) } by A4; :: thesis:

end;

let p be FinSequence of NAT ; :: thesis:
assume p 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:
then A5: 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 q being FinSequence of NAT such that
A6: q in C and
A7: p is_a_prefix_of q ;
thus ProperPrefixes p c= { w where w is Element of W : ex p being FinSequence of NAT st
( p in C & w is_a_prefix_of p ) } :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in ProperPrefixes p ; :: thesis:
then consider r being FinSequence such that
A8: x = r and
A9: r is_a_proper_prefix_of p by TREES_1:def 2;
r is_a_prefix_of p by A9;
then ( r is_a_prefix_of q & r in W ) by A5, A7, TREES_1:20;
hence 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 ) } by A6, A8; :: thesis:

end;

end;

then A10: X <> {} by A1, A2, A3;

let Z be set ; :: thesis:
assume that
A11: Z <> {} and
A12: Z c= X and
A13: Z is c=-linear ; :: thesis:
union Z c= W

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union Z ; :: thesis:
then consider Y being set such that
A14: x in Y and
A15: Y in Z by TARSKI:def 4;
Y in bool W by A1, A12, A15;
hence x in W by A14; :: thesis:

end;

then reconsider Z9 = union Z as Subset of W ;
A16: Z9 is Chain of W

let p be FinSequence of NAT ; :: according to TREES_2:def 3 :: thesis:
let q be FinSequence of NAT ; :: thesis:
assume p in Z9 ; :: thesis:
then consider X1 being set such that
A17: p in X1 and
A18: X1 in Z by TARSKI:def 4;
assume q in Z9 ; :: thesis:
then consider X2 being set such that
A19: q in X2 and
A20: X2 in Z by TARSKI:def 4;
X1,X2 are_c=-comparable by A13, A18, A20;
then A21: ( X1 c= X2 or X2 c= X1 ) ;
A22: X1 is Chain of W by A1, A12, A18;
X2 is Chain of W by A1, A12, A20;
hence p,q are_c=-comparable by A17, A19, A21, A22, Def3; :: thesis:

end;

A23: now :: thesis:

let p be FinSequence of NAT ; :: thesis:
assume p in union Z ; :: thesis:
then consider X1 being set such that
A24: ( p in X1 & X1 in Z ) by TARSKI:def 4;
( ProperPrefixes p c= X1 & X1 c= union Z ) by A1, A12, A24, ZFMISC_1:74;
hence ProperPrefixes p c= union Z ; :: thesis:

end;

set x = the Element of Z;
the Element of Z in X by A11, A12;
then A25: C c= the Element of Z by A1;
the Element of Z c= union Z by A11, ZFMISC_1:74;
then C c= union Z by A25;
hence union Z in X by A1, A16, A23; :: thesis:

end;

then consider Y being set such that
A26: Y in X and
A27: for Z being set st Z in X & Z <> Y holds
not Y c= Z by A10, ORDERS_1:67;
reconsider Y = Y as Chain of W by A1, A26;

thus for p being FinSequence of NAT st p in Y holds
ProperPrefixes p c= Y by A1, A26; :: thesis:
given p being FinSequence of NAT such that A28: p in W and
A29: for q being FinSequence of NAT st q in Y holds
q is_a_proper_prefix_of p ; :: thesis:
set Z = (ProperPrefixes p) \/ {p};
( ProperPrefixes p c= W & {p} c= W ) by A28, TREES_1:def 3, ZFMISC_1:31;
then reconsider Z9 = (ProperPrefixes p) \/ {p} as Subset of W by XBOOLE_1:8;
A30: Z9 is Chain of W

let q be FinSequence of NAT ; :: according to TREES_2:def 3 :: thesis:
let r be FinSequence of NAT ; :: thesis:
assume that
A31: q in Z9 and
A32: r in Z9 ; :: thesis:
A33: ( q in ProperPrefixes p or q in {p} ) by A31, XBOOLE_0:def 3;
A34: ( r in ProperPrefixes p or r in {p} ) by A32, XBOOLE_0:def 3;
A35: ( q is_a_proper_prefix_of p or q = p ) by A33, TARSKI:def 1, TREES_1:12;
A36: ( r is_a_proper_prefix_of p or r = p ) by A34, TARSKI:def 1, TREES_1:12;
A37: q is_a_prefix_of p by A35;
r is_a_prefix_of p by A36;
hence q,r are_c=-comparable by A37, Th1; :: thesis:

end;

A38: now :: thesis:

let q be FinSequence of NAT ; :: thesis:
assume q in (ProperPrefixes p) \/ {p} ; :: thesis:
then ( q in ProperPrefixes p or q in {p} ) by XBOOLE_0:def 3;
then ( q is_a_proper_prefix_of p or q = p ) by TARSKI:def 1, TREES_1:12;
then q is_a_prefix_of p ;
then A39: ProperPrefixes q c= ProperPrefixes p by TREES_1:17;
ProperPrefixes p c= (ProperPrefixes p) \/ {p} by XBOOLE_1:7;
hence ProperPrefixes q c= (ProperPrefixes p) \/ {p} by A39; :: thesis:

end;

A40: Y c= (ProperPrefixes p) \/ {p}

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A41: x in Y ; :: thesis:
then reconsider t = x as Element of W ;
t is_a_proper_prefix_of p by A29, A41;
then t in ProperPrefixes p by TREES_1:12;
hence x in (ProperPrefixes p) \/ {p} by XBOOLE_0:def 3; :: thesis:

end;

C c= Y by A1, A26;
then C c= (ProperPrefixes p) \/ {p} by A40;
then A42: (ProperPrefixes p) \/ {p} in X by A1, A30, A38;
A43: p in {p} by TARSKI:def 1;
A44: not p in Y by A29;
p in (ProperPrefixes p) \/ {p} by A43, XBOOLE_0:def 3;
hence contradiction by A27, A40, A42, A44; :: thesis:

end;

then reconsider Y = Y as Branch of W by Def7;
take Y ; :: thesis:
thus C c= Y by A1, A26; :: thesis: