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)
per cases ( i = j + 1 or j = i + 1 ) by A1;
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;
suppose j = i + 1 ; :: thesis: [i,j] in the InternalRel of (Necklace n)
hence [i,j] in the InternalRel of (Necklace n) by A3, Th20, Th21; :: thesis: verum
end;
end;