let n be Nat; :: thesis: for i, j being Nat st ( i = j + 1 or j = i + 1 ) & i in the carrier of (Necklace n) & j in the carrier of (Necklace n) holds

[i,j] in the InternalRel of (Necklace n)

let i, j be Nat; :: thesis: ( ( i = j + 1 or j = i + 1 ) & i in the carrier of (Necklace n) & j in the carrier of (Necklace n) implies [i,j] in the InternalRel of (Necklace n) )

assume that

A1: ( i = j + 1 or j = i + 1 ) and

A2: i in the carrier of (Necklace n) and

A3: j in the carrier of (Necklace n) ; :: thesis: [i,j] in the InternalRel of (Necklace n)

[i,j] in the InternalRel of (Necklace n)

let i, j be Nat; :: thesis: ( ( i = j + 1 or j = i + 1 ) & i in the carrier of (Necklace n) & j in the carrier of (Necklace n) implies [i,j] in the InternalRel of (Necklace n) )

assume that

A1: ( i = j + 1 or j = i + 1 ) and

A2: i in the carrier of (Necklace n) and

A3: j in the carrier of (Necklace n) ; :: thesis: [i,j] in the InternalRel of (Necklace n)

per cases
( i = j + 1 or j = i + 1 )
by A1;

end;

suppose A4:
i = j + 1
; :: thesis: [i,j] in the InternalRel of (Necklace n)

then
[j,(j + 1)] in the InternalRel of (Necklace n)
by A2, Th20, Th21;

then [(j + 1),j] in the InternalRel of (Necklace n) ~ by RELAT_1:def 7;

hence [i,j] in the InternalRel of (Necklace n) by A4, RELAT_2:13; :: thesis: verum

end;then [(j + 1),j] in the InternalRel of (Necklace n) ~ by RELAT_1:def 7;

hence [i,j] in the InternalRel of (Necklace n) by A4, RELAT_2:13; :: thesis: verum