let n be non zero Nat; Necklace n is connected
given X, Y being Subset of (Necklace n) such that A1:
X <> {}
and
A2:
Y <> {}
and
A3:
[#] (Necklace n) = X \/ Y
and
A4:
X misses Y
and
A5:
the InternalRel of (Necklace n) = ( the InternalRel of (Necklace n) |_2 X) \/ ( the InternalRel of (Necklace n) |_2 Y)
; ORDERS_3:def 2,ORDERS_3:def 3 contradiction
A6:
( the carrier of (Necklace n) = n & 0 in n )
by Th3, Th19;
per cases
( 0 in X or 0 in Y )
by A3, A6, XBOOLE_0:def 3;
suppose A7:
0 in X
;
contradictiondefpred S1[
Nat]
means $1
in Y;
consider x being
Element of
(Necklace n) such that A8:
x in Y
by A2, SUBSET_1:4;
x in the
carrier of
(Necklace n)
;
then
x in Segm n
by Th19;
then
x is
natural
;
then A9:
ex
x being
Nat st
S1[
x]
by A8;
consider k being
Nat such that A10:
S1[
k]
and A11:
for
i being
Nat st
S1[
i] holds
k <= i
from NAT_1:sch 5(A9);
k <> 0
by A4, A7, A10, XBOOLE_0:3;
then consider i being
Nat such that A12:
k = i + 1
by NAT_1:6;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
A13:
not
i in Y
by A11, A12, XREAL_1:29;
A14:
not
i + 1
in X
by A4, A10, A12, XBOOLE_0:3;
A15:
[i,(i + 1)] in the
InternalRel of
(Necklace n)
by A10, A12, Th20, Th21;
hence
contradiction
;
verum end; suppose A16:
0 in Y
;
contradictiondefpred S1[
Nat]
means $1
in X;
consider y being
Element of
(Necklace n) such that A17:
y in X
by A1, SUBSET_1:4;
y in the
carrier of
(Necklace n)
;
then
y in Segm n
by Th19;
then
y is
natural
;
then A18:
ex
y being
Nat st
S1[
y]
by A17;
consider k being
Nat such that A19:
S1[
k]
and A20:
for
i being
Nat st
S1[
i] holds
k <= i
from NAT_1:sch 5(A18);
k <> 0
by A4, A16, A19, XBOOLE_0:3;
then consider i being
Nat such that A21:
k = i + 1
by NAT_1:6;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
A22:
not
i in X
by A20, A21, XREAL_1:29;
A23:
not
i + 1
in Y
by A4, A19, A21, XBOOLE_0:3;
A24:
[i,(i + 1)] in the
InternalRel of
(Necklace n)
by A19, A21, Th20, Th21;
hence
contradiction
;
verum end;