let n be Nat; :: thesis: 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 }
set I = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ;
{ [i,(i + 1)] where i is Element of NAT : i + 1 < n } is Relation-like

proof

let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } or ex b₁, b₂ being object st x = [b₁,b₂] )
assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; :: thesis: ex b₁, b₂ being object st x = [b₁,b₂]
then ex i being Element of NAT st
( x = [i,(i + 1)] & i + 1 < n ) ;
hence ex b₁, b₂ being object st x = [b₁,b₂] ; :: thesis: verum

end;

then reconsider I = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } as Relation ;
set B = n -SuccRelStr ;
deffunc H₁( Element of NAT ) -> Element of NAT = $1;
deffunc H₂( Element of NAT ) -> Element of omega = $1 + 1;
defpred S₁[ Element of NAT ] means $1 + 1 < n;
set R = { [H₂(i),H₁(i)] where i is Element of NAT : S₁[i] } ;
A1: I = { [H₁(i),H₂(i)] where i is Element of NAT : S₁[i] } ;
A2: I ~ = { [H₂(i),H₁(i)] where i is Element of NAT : S₁[i] } from NECKLACE:sch 1(A1);
the InternalRel of (n -SuccRelStr) = I by Def6;
hence 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 A2, Def7; :: thesis: verum