let W be Tree; for C being Chain of W ex B being Branch of W st C c= B
let C be Chain of W; ex B being Branch of W st C c= B
defpred S1[ 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 & S1[Y] ) )
from XBOOLE_0: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 Th26;
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 ) }
A16:
X <> {}
by A1, A2, A3, A6;
A17:
now let Z be
set ;
( Z <> {} & Z c= X & Z is c=-linear implies union Z in X )assume that A18:
Z <> {}
and A19:
Z c= X
and A20:
Z is
c=-linear
;
union Z in XA21:
union Z c= W
reconsider Z9 =
union Z as
Subset of
W by A21;
A26:
Z9 is
Chain of
W
proof
let p be
FinSequence of
NAT ;
TREES_2:def 3 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 ;
( p in Z9 & q in Z9 implies p,q are_c=-comparable )
assume A27:
p in Z9
;
( not q in Z9 or p,q are_c=-comparable )
consider X1 being
set such that A28:
p in X1
and A29:
X1 in Z
by A27, TARSKI:def 4;
assume A30:
q in Z9
;
p,q are_c=-comparable
consider X2 being
set such that A31:
q in X2
and A32:
X2 in Z
by A30, TARSKI:def 4;
A33:
X1,
X2 are_c=-comparable
by A20, A29, A32, ORDINAL1:def 9;
A34:
(
X1 c= X2 or
X2 c= X1 )
by A33, XBOOLE_0:def 9;
A35:
X1 is
Chain of
W
by A1, A19, A29;
A36:
X2 is
Chain of
W
by A1, A19, A32;
thus
p,
q are_c=-comparable
by A28, A31, A34, A35, A36, Def3;
verum
end; consider x being
Element of
Z;
A41:
x in X
by A18, A19, TARSKI:def 3;
A42:
C c= x
by A1, A41;
A43:
x c= union Z
by A18, ZFMISC_1:92;
A44:
C c= union Z
by A42, A43, XBOOLE_1:1;
thus
union Z in X
by A1, A26, A37, A44;
verum end;
consider Y being set such that
A45:
Y in X
and
A46:
for Z being set st Z in X & Z <> Y holds
not Y c= Z
by A16, A17, ORDERS_1:177;
reconsider Y = Y as Chain of W by A1, A45;
A47:
now thus
for
p being
FinSequence of
NAT st
p in Y holds
ProperPrefixes p c= Y
by A1, A45;
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 A48:
p in W
and A49:
for
q being
FinSequence of
NAT st
q in Y holds
q is_a_proper_prefix_of p
;
contradictionset Z =
(ProperPrefixes p) \/ {p};
A50:
(
ProperPrefixes p c= W &
{p} c= W )
by A48, TREES_1:def 5, ZFMISC_1:37;
reconsider Z9 =
(ProperPrefixes p) \/ {p} as
Subset of
W by A50, XBOOLE_1:8;
A51:
Z9 is
Chain of
W
proof
let q be
FinSequence of
NAT ;
TREES_2:def 3 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 ;
( q in Z9 & r in Z9 implies q,r are_c=-comparable )
assume that A52:
q in Z9
and A53:
r in Z9
;
q,r are_c=-comparable
A54:
(
q in ProperPrefixes p or
q in {p} )
by A52, XBOOLE_0:def 3;
A55:
(
r in ProperPrefixes p or
r in {p} )
by A53, XBOOLE_0:def 3;
A56:
(
q is_a_proper_prefix_of p or
q = p )
by A54, TARSKI:def 1, TREES_1:36;
A57:
(
r is_a_proper_prefix_of p or
r = p )
by A55, TARSKI:def 1, TREES_1:36;
A58:
q is_a_prefix_of p
by A56, XBOOLE_0:def 8;
A59:
r is_a_prefix_of p
by A57, XBOOLE_0:def 8;
thus
q,
r are_c=-comparable
by A58, A59, Th1;
verum
end; A67:
Y c= (ProperPrefixes p) \/ {p}
A71:
C c= Y
by A1, A45;
A72:
C c= (ProperPrefixes p) \/ {p}
by A67, A71, XBOOLE_1:1;
A73:
(ProperPrefixes p) \/ {p} in X
by A1, A51, A60, A72;
A74:
p in {p}
by TARSKI:def 1;
A75:
not
p in Y
by A49;
A76:
p in (ProperPrefixes p) \/ {p}
by A74, XBOOLE_0:def 3;
thus
contradiction
by A46, A67, A73, A75, A76;
verum end;
reconsider Y = Y as Branch of W by A47, Def7;
take
Y
; C c= Y
thus
C c= Y
by A1, A45; verum