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 b1, b2 being object st x = [b1,b2] )
assume x in { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ; :: thesis: ex b1, b2 being object st x = [b1,b2]
then ex i being Element of NAT st
( x = [i,(i + 1)] & i + 1 < n ) ;
hence ex b1, b2 being object st x = [b1,b2] ; :: 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 H1( Element of NAT ) -> Element of NAT = $1;
deffunc H2( Element of NAT ) -> Element of omega = $1 + 1;
defpred S1[ Element of NAT ] means $1 + 1 < n;
set R = { [H2(i),H1(i)] where i is Element of NAT : S1[i] } ;
A1: I = { [H1(i),H2(i)] where i is Element of NAT : S1[i] } ;
A2: I ~ = { [H2(i),H1(i)] where i is Element of NAT : S1[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