let x be set ; :: according to NECKLACE:def 5 :: thesis: ( x in the carrier of (Necklace n) implies not [x,x] in the InternalRel of (Necklace n) )

set A = Necklace n;

assume x in the carrier of (Necklace n) ; :: thesis: not [x,x] in the InternalRel of (Necklace n)

A1: the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n } by Th17;

assume A2: [x,x] in the InternalRel of (Necklace n) ; :: thesis: contradiction

set A = Necklace n;

assume x in the carrier of (Necklace n) ; :: thesis: not [x,x] in the InternalRel of (Necklace n)

A1: the InternalRel of (Necklace n) = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } \/ { [(i + 1),i] where i is Element of NAT : i + 1 < n } by Th17;

assume A2: [x,x] in the InternalRel of (Necklace n) ; :: thesis: contradiction

per cases
( [x,x] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or [x,x] in { [(i + 1),i] where i is Element of NAT : i + 1 < n } )
by A2, A1, XBOOLE_0:def 3;

end;