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