defpred S1[ 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 & S1[Y] ) )
from XBOOLE_0:sch 1();
A2:
( {} is Chain of W & ( for p being FinSequence of NAT st p in {} holds
ProperPrefixes p c= {} ) )
by Th21;
A3:
X <> {}
by A1, A2;
A4:
now let Z be
set ;
( Z <> {} & Z c= X & Z is c=-linear implies union Z in X )assume that
Z <> {}
and A5:
Z c= X
and A6:
Z is
c=-linear
;
union Z in XA7:
union Z c= W
reconsider Z9 =
union Z as
Subset of
W by A7;
A12:
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 A13:
p in Z9
;
( not q in Z9 or p,q are_c=-comparable )
consider X1 being
set such that A14:
p in X1
and A15:
X1 in Z
by A13, TARSKI:def 4;
assume A16:
q in Z9
;
p,q are_c=-comparable
consider X2 being
set such that A17:
q in X2
and A18:
X2 in Z
by A16, TARSKI:def 4;
A19:
X1,
X2 are_c=-comparable
by A6, A15, A18, ORDINAL1:def 9;
A20:
(
X1 c= X2 or
X2 c= X1 )
by A19, XBOOLE_0:def 9;
A21:
X1 is
Chain of
W
by A1, A5, A15;
A22:
X2 is
Chain of
W
by A1, A5, A18;
thus
p,
q are_c=-comparable
by A14, A17, A20, A21, A22, Def3;
verum
end; thus
union Z in X
by A1, A12, A23;
verum end;
consider Y being set such that
A27:
Y in X
and
A28:
for Z being set st Z in X & Z <> Y holds
not Y c= Z
by A3, A4, ORDERS_1:177;
reconsider Y = Y as Chain of W by A1, A27;
take
Y
; Y is Branch-like
thus
for p being FinSequence of NAT st p in Y holds
ProperPrefixes p c= Y
by A1, A27; TREES_2:def 7 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 A29:
p in W
and
A30:
for q being FinSequence of NAT st q in Y holds
q is_a_proper_prefix_of p
; contradiction
set Z = (ProperPrefixes p) \/ {p};
A31:
( ProperPrefixes p c= W & {p} c= W )
by A29, TREES_1:def 5, ZFMISC_1:37;
reconsider Z9 = (ProperPrefixes p) \/ {p} as Subset of W by A31, XBOOLE_1:8;
A32:
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 A33:
q in Z9
and A34:
r in Z9
;
q,r are_c=-comparable
A35:
(
q in ProperPrefixes p or
q in {p} )
by A33, XBOOLE_0:def 3;
A36:
(
r in ProperPrefixes p or
r in {p} )
by A34, XBOOLE_0:def 3;
A37:
(
q is_a_proper_prefix_of p or
q = p )
by A35, TARSKI:def 1, TREES_1:36;
A38:
(
r is_a_proper_prefix_of p or
r = p )
by A36, TARSKI:def 1, TREES_1:36;
A39:
q is_a_prefix_of p
by A37, XBOOLE_0:def 8;
A40:
r is_a_prefix_of p
by A38, XBOOLE_0:def 8;
thus
q,
r are_c=-comparable
by A39, A40, Th1;
verum
end;
A48:
(ProperPrefixes p) \/ {p} in X
by A1, A32, A41;
A49:
p in {p}
by TARSKI:def 1;
A50:
not p in Y
by A30;
A51:
p in (ProperPrefixes p) \/ {p}
by A49, XBOOLE_0:def 3;
A52:
Y c= (ProperPrefixes p) \/ {p}
thus
contradiction
by A28, A48, A50, A51, A52; verum