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)
A2: 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 Th19;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
[j,(j + 1)] in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } by A1;
hence [j,(j + 1)] in the InternalRel of (Necklace n) by A2, XBOOLE_0:def 3; :: thesis: verum