let n, j be Nat; :: thesis: ( j + 1 < n implies [j,(j + 1)] in the InternalRel of (Necklace n) )

assume A1: j + 1 < n ; :: thesis: [j,(j + 1)] in the InternalRel of (Necklace n)

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A2: [j,(j + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by 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;

hence [j,(j + 1)] in the InternalRel of (Necklace n) by A2, XBOOLE_0:def 3; :: thesis: verum

assume A1: j + 1 < n ; :: thesis: [j,(j + 1)] in the InternalRel of (Necklace n)

reconsider j = j as Element of NAT by ORDINAL1:def 12;

A2: [j,(j + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by 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;

hence [j,(j + 1)] in the InternalRel of (Necklace n) by A2, XBOOLE_0:def 3; :: thesis: verum