let n be non zero Nat; :: thesis: 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) ; :: according to ORDERS_3:def 2,ORDERS_3:def 3 :: thesis: contradiction

A6: ( the carrier of (Necklace n) = n & 0 in n ) by Th3, Th19;

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 & 0 in n ) by Th3, Th19;

per cases
( 0 in X or 0 in Y )
by A3, A6, XBOOLE_0:def 3;

end;

suppose A7:
0 in X
; :: thesis: contradiction

defpred S_{1}[ 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 S_{1}[x]
by A8;

consider k being Nat such that

A10: S_{1}[k]
and

A11: for i being Nat st S_{1}[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;

end;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 S

consider k being Nat such that

A10: S

A11: for i being Nat st S

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;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( [i,(i + 1)] in the InternalRel of (Necklace n) |_2 X or [i,(i + 1)] in the InternalRel of (Necklace n) |_2 Y )
by A5, A15, XBOOLE_0:def 3;

end;

suppose
[i,(i + 1)] in the InternalRel of (Necklace n) |_2 X
; :: thesis: contradiction

then
[i,(i + 1)] in [:X,X:]
by XBOOLE_0:def 4;

hence contradiction by A14, ZFMISC_1:87; :: thesis: verum

end;hence contradiction by A14, ZFMISC_1:87; :: thesis: verum

suppose
[i,(i + 1)] in the InternalRel of (Necklace n) |_2 Y
; :: thesis: contradiction

then
[i,(i + 1)] in [:Y,Y:]
by XBOOLE_0:def 4;

hence contradiction by A13, ZFMISC_1:87; :: thesis: verum

end;hence contradiction by A13, ZFMISC_1:87; :: thesis: verum

suppose A16:
0 in Y
; :: thesis: contradiction

defpred S_{1}[ 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 S_{1}[y]
by A17;

consider k being Nat such that

A19: S_{1}[k]
and

A20: for i being Nat st S_{1}[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;

end;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 S

consider k being Nat such that

A19: S

A20: for i being Nat st S

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;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( [i,(i + 1)] in the InternalRel of (Necklace n) |_2 Y or [i,(i + 1)] in the InternalRel of (Necklace n) |_2 X )
by A5, A24, XBOOLE_0:def 3;

end;

suppose
[i,(i + 1)] in the InternalRel of (Necklace n) |_2 Y
; :: thesis: contradiction

then
[i,(i + 1)] in [:Y,Y:]
by XBOOLE_0:def 4;

hence contradiction by A23, ZFMISC_1:87; :: thesis: verum

end;hence contradiction by A23, ZFMISC_1:87; :: thesis: verum

suppose
[i,(i + 1)] in the InternalRel of (Necklace n) |_2 X
; :: thesis: contradiction

then
[i,(i + 1)] in [:X,X:]
by XBOOLE_0:def 4;

hence contradiction by A22, ZFMISC_1:87; :: thesis: verum

end;hence contradiction by A22, ZFMISC_1:87; :: thesis: verum