defpred S₁[ set ] means ( W is Chain of W & ( for p being FinSequence of NAT st p in W holds
ProperPrefixes p c= W ) );
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();
( {} is Chain of W & ( for p being FinSequence of NAT st p in {} holds
ProperPrefixes p c= {} ) ) by Th19;
then A2: X <> {} by A1;

now :: thesis: for Z being set st Z <> {} & Z c= X & Z is c=-linear holds
union Z in X

let Z be set ; :: thesis: ( Z <> {} & Z c= X & Z is c=-linear implies union Z in X )
assume that
Z <> {} and
A3: Z c= X and
A4: Z is c=-linear ; :: thesis: union Z in X
union Z c= W

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union Z or x in W )
assume x in union Z ; :: thesis: x in W
then consider Y being set such that
A5: x in Y and
A6: Y in Z by TARSKI:def 4;
Y in bool W by A1, A3, A6;
hence x in W by A5; :: thesis: verum

end;

then reconsider Z9 = union Z as Subset of W ;
A7: Z9 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 Z9 & q in Z9 holds
p,q are_c=-comparable
let q be FinSequence of NAT ; :: thesis: ( p in Z9 & q in Z9 implies p,q are_c=-comparable )
assume p in Z9 ; :: thesis: ( not q in Z9 or p,q are_c=-comparable )
then consider X1 being set such that
A8: p in X1 and
A9: X1 in Z by TARSKI:def 4;
assume q in Z9 ; :: thesis: p,q are_c=-comparable
then consider X2 being set such that
A10: q in X2 and
A11: X2 in Z by TARSKI:def 4;
X1,X2 are_c=-comparable by A4, A9, A11;
then A12: ( X1 c= X2 or X2 c= X1 ) ;
A13: X1 is Chain of W by A1, A3, A9;
X2 is Chain of W by A1, A3, A11;
hence p,q are_c=-comparable by A8, A10, A12, A13, Def3; :: thesis: verum

end;

now :: thesis: for p being FinSequence of NAT st p in union Z holds
ProperPrefixes p c= union Z

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

end;

hence union Z in X by A1, A7; :: thesis: verum

end;

then consider Y being set such that
A15: Y in X and
A16: for Z being set st Z in X & Z <> Y holds
not Y c= Z by A2, ORDERS_1:67;
reconsider Y = Y as Chain of W by A1, A15;
take Y ; :: thesis: Y is Branch-like
thus for p being FinSequence of NAT st p in Y holds
ProperPrefixes p c= Y by A1, A15; :: according to TREES_2:def 7 :: thesis: for p being FinSequence of NAT holds
( not p in W or ex q being FinSequence of NAT st
( q in Y & not q is_a_proper_prefix_of p ) )
given p being FinSequence of NAT such that A17: p in W and
A18: for q being FinSequence of NAT st q in Y holds
q is_a_proper_prefix_of p ; :: thesis: contradiction
set Z = (ProperPrefixes p) \/ {p};
( ProperPrefixes p c= W & {p} c= W ) by A17, TREES_1:def 3, ZFMISC_1:31;
then reconsider Z9 = (ProperPrefixes p) \/ {p} as Subset of W by XBOOLE_1:8;
A19: Z9 is Chain of W

proof

let q be FinSequence of NAT ; :: according to TREES_2:def 3 :: thesis: for q being FinSequence of NAT st q in Z9 & q in Z9 holds
q,q are_c=-comparable
let r be FinSequence of NAT ; :: thesis: ( q in Z9 & r in Z9 implies q,r are_c=-comparable )
assume that
A20: q in Z9 and
A21: r in Z9 ; :: thesis: q,r are_c=-comparable
A22: ( q in ProperPrefixes p or q in {p} ) by A20, XBOOLE_0:def 3;
A23: ( r in ProperPrefixes p or r in {p} ) by A21, XBOOLE_0:def 3;
A24: ( q is_a_proper_prefix_of p or q = p ) by A22, TARSKI:def 1, TREES_1:12;
A25: ( r is_a_proper_prefix_of p or r = p ) by A23, TARSKI:def 1, TREES_1:12;
A26: q is_a_prefix_of p by A24;
r is_a_prefix_of p by A25;
hence q,r are_c=-comparable by A26, Th1; :: thesis: verum

end;

now :: thesis: for q being FinSequence of NAT st q in (ProperPrefixes p) \/ {p} holds
ProperPrefixes q c= (ProperPrefixes p) \/ {p}

let q be FinSequence of NAT ; :: thesis: ( q in (ProperPrefixes p) \/ {p} implies ProperPrefixes q c= (ProperPrefixes p) \/ {p} )
assume q in (ProperPrefixes p) \/ {p} ; :: thesis: ProperPrefixes q c= (ProperPrefixes p) \/ {p}
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 A27: 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 A27; :: thesis: verum

end;

then A28: (ProperPrefixes p) \/ {p} in X by A1, A19;
A29: p in {p} by TARSKI:def 1;
A30: not p in Y by A18;
A31: p in (ProperPrefixes p) \/ {p} by A29, XBOOLE_0:def 3;
Y c= (ProperPrefixes p) \/ {p}

proof

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

end;

hence contradiction by A16, A28, A30, A31; :: thesis: verum