let n be non empty Nat; :: thesis: not Necklace n is parallel
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)
; :: according to ORDERS_3:def 2,ORDERS_3:def 3 :: thesis: contradiction
A6:
the carrier of (Necklace n) = n
by Th21;
A7:
0 in n
by Th5;
per cases
( 0 in X or 0 in Y )
by A3, A6, A7, XBOOLE_0:def 3;
suppose A8:
0 in X
;
:: thesis: contradictiondefpred S1[
Nat]
means $1
in Y;
consider x being
Element of
(Necklace n) such that A9:
x in Y
by A2, SUBSET_1:10;
x in the
carrier of
(Necklace n)
;
then
x in n
by Th21;
then
x is
natural
by Th4;
then A10:
ex
x being
Nat st
S1[
x]
by A9;
consider k being
Nat such that A11:
S1[
k]
and A12:
for
i being
Nat st
S1[
i] holds
k <= i
from NAT_1:sch 5(A10);
k <> 0
by A4, A8, A11, XBOOLE_0:3;
then consider i being
Nat such that A13:
k = i + 1
by NAT_1:6;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
A14:
not
i in Y
by A12, A13, XREAL_1:31;
A15:
not
i + 1
in X
by A4, A11, A13, XBOOLE_0:3;
A16:
[i,(i + 1)] in the
InternalRel of
(Necklace n)
by A11, A13, Th22, Th23;
hence
contradiction
;
:: thesis: verum end; suppose A17:
0 in Y
;
:: thesis: contradictiondefpred S1[
Nat]
means $1
in X;
consider y being
Element of
(Necklace n) such that A18:
y in X
by A1, SUBSET_1:10;
y in the
carrier of
(Necklace n)
;
then
y in n
by Th21;
then
y is
natural
by Th4;
then A19:
ex
y being
Nat st
S1[
y]
by A18;
consider k being
Nat such that A20:
S1[
k]
and A21:
for
i being
Nat st
S1[
i] holds
k <= i
from NAT_1:sch 5(A19);
k <> 0
by A4, A17, A20, XBOOLE_0:3;
then consider i being
Nat such that A22:
k = i + 1
by NAT_1:6;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 13;
A23:
not
i in X
by A21, A22, XREAL_1:31;
A24:
not
i + 1
in Y
by A4, A20, A22, XBOOLE_0:3;
A25:
[i,(i + 1)] in the
InternalRel of
(Necklace n)
by A20, A22, Th22, Th23;
hence
contradiction
;
:: thesis: verum end;